proposition: Lemma mx_lang_Union_spec: forall M', mx_lang_Union <== M' <-> forall i, M i <== M'.
proof: Proof. Opaque leq. intros. split. intros H u. rewrite <- H. unfold mx_lang_Union. rewrite (mx_leq_pointwise (G:=@lang_Graph label)). intros s t Hs Ht. simpl. rewrite <- leq_lang_Union. reflexivity. intro H. rewrite (mx_leq_pointwise (G:=@lang_Graph label)). intros s t Hs Ht. simpl. rewrite -> lang_Union_spec. intro u. apply (H u _ _ Hs Ht). Transparent leq. Qed.
imports: Coq(List) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(Functors) ATBR(MxFunctors) ATBR(DKA_Definitions) ATBR(Model_Languages)