proposition: Lemma matches_correct : forall p t u, matches p t = Some u -> t = p ++ u.
proof: Proof. induction p; simpl; intros. inversion H. refl. destruct t. discr. revert H. case_beq_symb a s. 2: discr. intro. rewrite (IHp _ _ H). refl. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(LogicUtil Srs ListUtil EqUtil RelUtil ListDec NatUtil)