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