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