proposition: Lemma remove_update : forall x E F, ok E -> (E ::= F) ∖ {x} = (E ∖ {x}) ::= F.
proof: Proof. intros. induction F as [ | (y, v) F IHF ]; simpl; auto. rewrite <- IHF. apply remove_update_one. apply ok_update; auto. Qed.
imports: Utf8 Equalities