fact: Definition rwr_subst R sigma' sigma := trans_clos (D.multiset_extension_step (fun yval' xval => rwr R (snd yval') (snd xval))) sigma' sigma.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)