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