-and subst delift_by_one what (with_what : nf) (where : nf) =
- let aux_propagate_arity ar = function
- | `Lam(false,`Match(`I(v,args),(x,_),liftno,bs,args')) ->
- `Lam(false,`Match(`I(v,args),(x,ar),liftno,bs,args'))
+and subst truelam delift_by_one what (with_what : nf) (where : nf) =
+ let rec aux_propagate_arity ar = function
+ | `Lam(false, t) when not delift_by_one -> `Lam(false, aux_propagate_arity ar t)
+ | `Match(`I(v,args),(x,_),liftno,bs,args') when not delift_by_one ->
+ `Match(`I(v,args),(x,ar),liftno,bs,args')
+ | `Var(i,oldar) -> `Var(i, if truelam then (assert (oldar = min_int); ar) else oldar)