proposition: Lemma update_one_concat_ok : forall E F x v, ok (E & F) -> (E & F) [x <- v] = (E [x <- v]) & (F [x <- v]).
proof: Proof. intros E F x v Hok. induction F as [ | (y, w) F IHF ]; simpl in *; auto. inversion Hok as [ | z w' G Hok2 ]; subst. destruct Hok2 as [ Hok2 Hnotin ]. rewrite IHF; auto. destruct (eq_keys_dec x y); subst; simpl; auto. rewrite update_one_notin; auto. apply notin_concat_inv in Hnotin. destruct Hnotin; auto. Qed.
imports: Utf8 Equalities