fact: Definition subst_of_matching (m : matching) := fun (x : variable) => \unopt_(Var x) (VM.find x m).
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)