- `Match (t,ar,bs_lift,bs,args))
- | `I _ | `Var _ | `Match _ -> `Match(t,ar,bs_lift,bs,args)
-
-and subst delift_by_one what (with_what : nf) (where : nf) =
+ `Match (t,(n,ar),bs_lift,bs,args))
+ | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,args)
+
+and subst truelam 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')) when not delift_by_one ->
+ `Lam(false,`Match(`I(v,args),(x,ar),liftno,bs,args'))
+ | `Var(i,oldar) -> `Var(i, if truelam && oldar = min_int then ar else oldar)
+ | _ as t -> t in