(* 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. *)
(* 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. *)