+(* 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
+