- `Match (t,(n,ar),bs_lift,bs,args))
- | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,args)
-
-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'))
+ `Match (t,(n,ar),bs_lift,bs,[]))
+ (* We are assuming that the econding of matches is s.t.:
+ - match PAC.. --> PAC
+ - match BOT.. --> BOT *)
+ | `Bottom -> `Bottom
+ | `Pacman -> `Pacman
+ | `Lam _ -> assert false
+ | `I _ | `Var _ | `Match _ as t -> `Match(t,(n,ar),bs_lift,bs,[]) in
+ mk_appl m args
+
+and subst truelam delift_by_one what (with_what : nf(*_nob*)) (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)