proposition: Lemma remove_ok_notin : forall x E, ok E -> x ∉ (E ∖ {x}).
proof: Proof. intros x E Hok. induction E as [ | (y, v) E IHE]; simpl. apply notin_empty. inversion Hok as [ | z w F Hok2 ]; subst. destruct Hok2 as [ Hok2 Hnotin ]. apply IHE in Hok2. destruct (eq_keys_dec x y); subst; auto. assert (x ∉ (E ∖ {x}) & y ∶ v); auto. apply notin_concat; auto. apply notin_single; auto. Qed.
imports: Utf8 Equalities