proposition: Lemma notin_remove_notin : forall x y E, x ∉ E -> x ∉ (E ∖ {y}).
proof: Proof. intros x y E Hnotin. induction E as [ | (z, v) E IHE ]; simpl; auto. assert (x ∉ E & (z ∶ v)) as Hnotin2 by auto. clear Hnotin. apply notin_concat_inv in Hnotin2. destruct Hnotin2 as [ Hnotin Hnotin2 ]. apply notin_single_inv in Hnotin2. destruct (eq_keys_dec y z) as [ Heq | Hneq ]; auto. apply IHE in Hnotin. assert (x ∉ (E ∖ {y}) & (z ∶ v)); auto. apply notin_concat; auto. apply notin_single; auto. Qed.
imports: Utf8 Equalities