(* as lift but lifts only indexes >= from *)
val lift_from: int -> int -> Cic.term -> Cic.term
-(* subst t1 t2 *)
-(* substitutes [t1] for [Rel 1] in [t2] *)
-val subst : Cic.term -> Cic.term -> Cic.term
+(* subst t1 t2 *)
+(* substitutes [t1] for [Rel 1] in [t2] *)
+(* if avoid_beta_redexes is true (default: false) no new beta redexes *)
+(* are generated. WARNING: the substitution can diverge when t2 is not *)
+(* well typed and avoid_beta_redexes is true. *)
+val subst : ?avoid_beta_redexes:bool -> Cic.term -> Cic.term -> Cic.term
(* subst_vars exp_named_subst t2 *)
(* applies [exp_named_subst] to [t2] *)