(* lift n t *)
(* lifts [t] of [n] *)
(* [from] default 1, lifts only indexes >= [from] *)
(* NOTE: the opposite function (delift_rels) is defined in CicMetaSubst *)
(* since it needs to restrict the metavariables in case of failure *)
(* lift n t *)
(* lifts [t] of [n] *)
(* [from] default 1, lifts only indexes >= [from] *)
(* NOTE: the opposite function (delift_rels) is defined in CicMetaSubst *)
(* since it needs to restrict the metavariables in case of failure *)
(* are generated. WARNING: the substitution can diverge when t2 is not *)
(* well typed and avoid_beta_redexes is true. *)
val subst :
(* are generated. WARNING: the substitution can diverge when t2 is not *)
(* well typed and avoid_beta_redexes is true. *)
val subst :
* the function is ReductionStrategy.from_env_for_unwind when psubst is
* used to implement nCicReduction.unwind' *)
val psubst :
* the function is ReductionStrategy.from_env_for_unwind when psubst is
* used to implement nCicReduction.unwind' *)
val psubst :
(* 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 *)
(* subst_meta (n, Irl _) t -> lift 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 *)
(* subst_meta (n, Irl _) t -> lift n t *)