proposition: Lemma exmatches_var_min : forall y t θ θ', exmatch θ y t = Some θ' -> forall x, VM.mem x θ' = VM.mem x θ || (y =X x).
proof: Proof. intros y t θ θ'; unfold exmatch; case_eq (VM.find y θ). intros v H; case (t =T v); intros Htu; try discr. inversion_clear Htu in H; intros x; case_eq (y =X x); intros Hxy. by rewrite <- (proj1 (beq_nat_ok _ _) Hxy), VMF.mem_find_b, H. by rewrite orb_false_r. intros Hymem H x; inversion_clear H in Hymem; case_eq (y =X x). intros Hxy; rewrite (proj1 (beq_nat_ok _ _) Hxy), VMF.add_b, orb_comm; unfold VMF.eqb; unfold VMF.eq_dec. by rewrite (eq_nat_dec_refl x). intros Hxy; rewrite VMF.add_b. by rewrite orb_comm, vmap_eqb, Hxy. Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)