proposition: Lemma mod_rewrite_correct : forall t mds u, mod_rewrite t mds = 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). ded (rewrite_correct H0). exists (last l t); split. apply FS_rtc. hyp. hyp. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(Srs LogicUtil SLoop ListUtil NatUtil RelUtil)