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