-;;
-
-(* apply_subst_reducing subst (Some (mtr,reductions_no)) t *)
-(* performs as (apply_subst subst t) until it finds an application of *)
-(* (META [meta_to_reduce]) that, once unwinding is performed, creates *)
-(* a new beta-redex; in this case up to [reductions_no] consecutive *)
-(* beta-reductions are performed. *)
-(* Hint: this function is usually called when [reductions_no] *)
-(* eta-expansions have been performed and the head of the new *)
-(* application has been unified with (META [meta_to_reduce]): *)
-(* during the unwinding the eta-expansions are undone. *)
-
-let apply_subst_reducing meta_to_reduce =