(* well typed and avoid_beta_redexes is true. *)
val subst : ?avoid_beta_redexes:bool -> NCic.term -> NCic.term -> NCic.term
(* well typed and avoid_beta_redexes is true. *)
val subst : ?avoid_beta_redexes:bool -> NCic.term -> NCic.term -> NCic.term
* [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 :
* [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 :