proposition: Lemma matches_r_dom : forall u t m m' x, matches_r u t m = Some m' -> ~In x (ATerm.vars u) -> VM.mem x m' = VM.mem x m.
proof: Proof. cut ((forall u t m m', matches_r u t m = Some m' -> forall x, ~In x (ATerm.vars u) -> VM.mem x m' = VM.mem x m) /\ (forall nu (us : terms nu) nt (ts : terms nt) m m', Vfold2 m matches_r us ts = Some m' -> forall x, ~In x (ATerm.vars_vec us) -> VM.mem x m' = VM.mem x m)). intuition. eapply H0. apply H. hyp. apply matches_some_ind. simpl. intuition. unfold exmatch in H. destruct (VM.find (elt:=term) x θ). revert H. case (beq_term t t0); intro. inversion H. refl. discr. inversion H. rewrite VMF.add_b. rewrite vmap_eqb. change (x<>x0) in H1. rewrite <- (beq_ko beq_nat_ok) in H1. rewrite H1. refl. intros. apply H0. rewrite vars_fun in H2. hyp. refl. simpl. intros. rewrite notin_app in H3. destruct H3. trans (VM.mem (elt:=term) x Ω). apply H0. hyp. apply H2. hyp. Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)