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