proposition: Lemma matches_dom : forall u t s x, matches u t = Some s -> ~In x (ATerm.vars u) -> s x = Var x.
proof: Proof. intros u t s x. unfold matches. case_eq (matches_r u t VM.empty). intros t0 H H0 H1. inversion H0. ded (matches_r_dom H H1). rewrite VMF.empty_a in H2. unfold subst_of_matching. revert H2. rewrite VMF.mem_find_b. destruct (VM.find x t0). discr. refl. discr. Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)