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