fact: Parameter one_step_apply_subst : forall R t1 t2 sigma , one_step R t1 t2 -> one_step R (apply_subst sigma t1) (apply_subst sigma t2).
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec)