proposition: Lemma ok_concat_comm : forall E F, ok (E & F) -> ok (F & E).
proof: Proof. intros E F Hok. apply ok_concat_inv in Hok. destruct Hok as [ HokE [ HokF [ HdomE HdomF ] ] ]. apply ok_concat; auto. Qed.
imports: Utf8 Equalities