proposition: Lemma matches_complete : forall p t u, t = p ++ u -> matches p t = Some u.
proof: Proof. induction p; simpl; intros; subst. refl. rewrite (beq_refl (@beq_symb_ok Sig)). apply IHp. refl. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(LogicUtil Srs ListUtil EqUtil RelUtil ListDec NatUtil)