proposition: Lemma update_one_concat_r : forall x v E F, x ∈ F -> (E & F) [x <- v] = E & (F [x <- v]).
proof: Proof. intros x v E F Hin. induction F as [ | (y, w) F IHF ]; simpl in *; auto. inversion Hin. destruct (eq_keys_dec x y) as [ Heq | Hneq ]; simpl in *; auto. unfold belongs in Hin. simpl in Hin. destruct Hin as [ Heq | Hin ]. elim Hneq; auto. f_equal; auto. Qed.
imports: Utf8 Equalities