proposition: Lemma ok_concat_inv : forall E F, ok (E & F) -> ok E ∧ ok F ∧ (dom E) ⊄ F ∧ (dom F) ⊄ E.
proof: Proof. intros E F Hok. induction F as [ | (x, v) F IHF ]; simpl in *. split; auto. split. apply ok_empty. split. apply all_notin_empty_r. unfold all_notin; intros; contradiction. inversion Hok as [ | y w G Hok2]; subst. destruct Hok2 as [ Hok2 Hnotin ]. apply IHF in Hok2. destruct Hok2 as [ HokE [ HokF [ HdomE HdomF ] ] ]. apply notin_concat_inv in Hnotin. destruct Hnotin as [ HnotinE HnotinF ]. split; auto. split. assert (ok (F & x ∶ v)); auto. apply ok_cons. split; auto. split. assert (dom E ⊄ F & x ∶ v); auto. apply all_notin_concat; auto. unfold all_notin. intros. apply notin_single. intro; subst. contradiction. unfold all_notin in *. intros y Hin. simpl in Hin. destruct Hin; subst; auto. Qed.
imports: Utf8 Equalities