proposition: Lemma mod_rewrite_correct : forall t dm u, mod_rewrite t dm = Some u -> red_mod E R t u.
proof: Proof. intros t [ds d] u. unfold mod_rewrite. case_eq (rewrites E t ds); intros. 2: discr. ded (rewrites_correct H). exists (last l t). split. apply FS_rtc. hyp. apply rewrite_correct with (d:=d). hyp. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(ATrs LogicUtil ALoop ListUtil RelUtil NatUtil APosition AMatching ARelation)