proposition: Lemma update_concat_l : forall E F G, ok (E & F) -> (E & F) ::= G = (E ::= G) & (F ::= G).
proof: Proof. intros E F G Hok. induction G as [ | (x, v) G IHG ]; simpl in *; auto. rewrite IHG. apply update_one_concat_ok. apply ok_concat_inv in Hok. destruct Hok as [ HokE [ HokF [ HdomE HdomF ] ] ]. assert (ok (E ::= G)) by (apply ok_update; auto). assert (ok (F ::= G)) by (apply ok_update; auto). apply ok_concat; auto; rewrite dom_update; apply all_notin_update; auto. Qed.
imports: Utf8 Equalities