proposition: Lemma belongs_remove : forall x y E, x <> y -> x ∈ E -> x ∈ (E ∖ {y}).
proof: Proof. induction E as [ | (z, v) E IHE ]; intros Hneq Hin; simpl in *; auto. assert (x ∈ E & (z ∶ v)) as Hin2 by auto; clear Hin. apply belongs_concat_inv in Hin2. destruct Hin2 as [ Hin | Hin ]; destruct (eq_keys_dec y z) as [ Heq | Hneq2 ]; subst; auto. assert (x ∈ (E ∖ {y}) & (z ∶ v)) as Hin2; auto. apply belongs_concat_l; auto. apply belongs_single_inv in Hin. contradiction. assert (x ∈ (E ∖ {y}) & (z ∶ v)); auto. apply belongs_concat_r; auto. Qed.
imports: Utf8 Equalities