proposition: Lemma update_notin : forall E F, (dom F) ⊄ E -> E ::= F = E.
proof: Proof. induction F as [ | (x, v) F IHF ]; unfold all_belongs; intro Hdom; simpl in *; auto. apply all_notin_notin in Hdom. destruct Hdom as [ Hnotin Hdom ]. apply IHF in Hdom. rewrite Hdom. apply update_one_notin; auto. Qed.
imports: Utf8 Equalities