proposition: Lemma subst_of_matchingE : forall x m v, VM.find x m = Some v -> \S(m) x = v.
proof: Proof. by intros x m v H; unfold subst_of_matching; rewrite H. Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)