+ (* Warning! It now applies again the substitution in branches of matches.
+ But careful, it does it many times, for every occurrence of
+ the match. This is okay because what does not occur in with_what. *)
+ let l' = l - bs_lift in
+ let with_what' = lift l' (with_what :> nf) in