fact: Fixpoint matches_r (u t : term) (m : matching) : option matching := match u, t with | Var y , _ => exmatch m y t | Fun g us, Fun f ts => if f =S g then Vfold2 m matches_r us ts else None | _ , _ => None end.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)