proposition: Lemma rewrite_correct : forall t d s, rewrite t d = Some s -> red R t s.
proof: Proof. intros t [p [l r]] s. unfold rewrite. case_eq (mem (@beq_rule Sig) (mkRule l r) R); intros. 2: discr. revert H0. case_eq (split t p); intros. destruct p0 as [u v]. 2: discr. revert H1. case_eq (matches l v); intros. rename s0 into w. 2: discr. exists l. exists r. exists (mkContext u w). unfold fill. simpl. inversion H2. intuition. rewrite mem_ok in H. hyp. apply beq_rule_ok. ded (matches_correct H1). ded (split_correct H0). subst. refl. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(LogicUtil Srs ListUtil EqUtil RelUtil ListDec NatUtil)