fact: Definition matches (u t : term) := match matches_r u t VM.empty with | None => None | Some m => Some \S(m) end.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)