proposition: Lemma belongs_remove_inv : forall x y E, ok E -> x ∈ (E ∖ {y}) -> x <> y.
proof: Proof. intros x y E Hok Hbelongs Heq; subst. induction E as [ | (x, v) E IHE ]; simpl in *; auto. inversion Hok as [ | z w F Hok2 ]; subst. destruct Hok2 as [ Hok2 Hnotin ]. destruct (eq_keys_dec y x) as [ Heq | Hneq ]; subst. contradiction. assert (y ∈ ((E ∖ {y}) & (x ∶ v))) as Hin by auto. clear Hbelongs. apply belongs_concat_inv in Hin. destruct Hin as [ | Hin ]; auto. apply belongs_single_inv in Hin; auto. Qed.
imports: Utf8 Equalities