(* well typed and avoid_beta_redexes is true. *)
val subst : ?avoid_beta_redexes:bool -> NCic.term -> NCic.term -> NCic.term
+(* psubst [avoid] [delift] [lift_args] [t] [map_arg] [args]
+ * [avoid] : do not leave newly created beta-redexes, default false
+ * [delift] : perform delifting
+ * [t] : term to fill in
+ * [lift_args] : lift argument after map_arg is applied
+ * [args] : stuff to substitute
+ * [map_arg] : map the argument to obtain a term
+ * the function is ReductionStrategy.from_env_for_unwind when psubst is
+ * used to implement nCicReduction.unwind' *)
+val psubst :
+ ?avoid_beta_redexes:bool -> bool -> int ->
+ ('a -> NCic.term) -> 'a list -> NCic.term ->
+ NCic.term
+
(* subst_meta (n, Ctx [t_1 ; ... ; t_n]) t *)
(* returns the term [t] where [Rel i] is substituted with [t_i] lifted by n *)
(* [t_i] is lifted as usual when it crosses an abstraction *)