proposition: Lemma rewrites_correct : forall ds t us, rewrites t ds = Some us -> FS t us.
proof: Proof. induction ds; simpl; intros. inversion H. exact I. revert H. case_eq (rewrite t a); intros. 2: discr. revert H0. case_eq (rewrites s ds); intros. 2: discr. inversion H1. simpl. ded (rewrite_correct H). intuition. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(LogicUtil Srs ListUtil EqUtil RelUtil ListDec NatUtil)