+(* 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. *)
+let rec subst ?(avoid_beta_redexes=false) arg =