proposition: Lemma rewrite_correct : forall t d u, rewrite t d = Some u -> red R t u.
proof: Proof. intros t [p [l r]] u. unfold rewrite. case_eq (mem beq_rule (mkRule l r) R); intros. 2: discr. revert H0. case_eq (subterm_pos t p); intros. 2: discr. revert H1. case_eq (matches l t0); intros. rename t1 into s. 2: discr. rewrite red_pos_ok. ex p l r s. split_all. rewrite mem_ok in H. hyp. apply beq_rule_ok. ded (matches_correct H1). rewrite H3. hyp. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(LogicUtil ATrs ListUtil RelUtil AMatching ListDec APosition NatUtil)