proposition: Lemma dom_update_one : forall x v E, dom (E [x <- v]) = dom E.
proof: Proof. intros x v. induction E as [ | (y, w) E IHE ]; simpl in *; auto. destruct (eq_keys_dec x y) as [ Heq | Hneq ]; simpl in *; auto. f_equal; auto. Qed.
imports: Utf8 Equalities