proposition: Lemma mod_rewrites_correct : forall mds t us, mod_rewrites t mds = Some us -> mod_FS t us.
proof: Proof. induction mds; simpl; intros. inversion H. exact I. revert H. case_eq (mod_rewrite t a); intros. 2: discr. revert H0. case_eq (mod_rewrites s mds); intros. 2: discr. inversion H1. simpl. ded (mod_rewrite_correct H). intuition. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(Srs LogicUtil SLoop ListUtil NatUtil RelUtil)