At the very very end of section 4, is it worth mentioning that in the Henglein/Tolmach/Oliva flow, all the >='s in the safety constraints are replaced with = except for condition 2. I.e., you perform one transformation on evaluating lambda's, but no coercions after that.