fact: Parameter rwr_apply_subst : forall R t1 t2 sigma, rwr R t1 t2 -> rwr 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)