fact: Fixpoint matches (p t : string) : option string := match p, t with | nil, _ => Some t | a :: p', b :: t' => if beq_symb a b then matches p' t' else None | _, _ => None end.
imports: Coq(Euclid Wf_nat) CoLoR(LogicUtil Srs ListUtil EqUtil RelUtil ListDec NatUtil)