proposition: Lemma remove_update_one : forall x y v E, ok E -> (update_one E y v) ∖ {x} = update_one (E ∖ {x}) y v.
proof: Proof. intros x y v E Hok. induction E as [ | (z, w) E IHE]; simpl in *; auto. inversion Hok as [ | z' w' F Hok2 ]; subst. destruct Hok2 as [ Hok2 Hnotin ]. apply IHE in Hok2. destruct (eq_keys_dec x z); subst. destruct (eq_keys_dec y z); simpl; destruct (eq_keys_dec y z); simpl; rewrite ?eq_keys_true; subst; try congruence. rewrite update_one_notin in *; auto. destruct (eq_keys_dec y z); simpl; destruct (eq_keys_dec y z); simpl; destruct (eq_keys_dec x z); subst; simpl; try congruence. Qed.
imports: Utf8 Equalities