proposition: Lemma ok_concat : forall E F, ok E -> ok F -> (dom E) ⊄ F -> (dom F) ⊄ E -> ok (E & F).
proof: Proof. intros E F HokE HokF HdomE HdomF. induction F as [ | (x, v) F IHF ]; simpl in *; auto. apply all_notin_notin in HdomF. destruct HdomF as [ HnotinE HdomF ]. inversion HokF as [ | y w G HokF2 ]; subst. destruct HokF2 as [ HokF2 HnotinF ]. assert (dom E ⊄ F & x ∶ v) as HdomE2 by auto. clear HdomE. apply all_notin_concat_inv in HdomE2. destruct HdomE2 as [ HdomE HdomE2 ]. apply all_notin_single_inv in HdomE2. assert (ok ((E & F) & (x ∶ v))); auto. apply ok_cons. split. apply IHF; auto. apply notin_concat; auto. Qed.
imports: Utf8 Equalities