proposition: Lemma lang_Union_spec I (L: I -> LX): forall L': LX, (lang_Union L: LX) <== L' <-> forall i, L i <== L'.
proof: Proof. intros. split; intro H. intro j. rewrite <- H. apply <- lang_leq. intros w Hw. exists j; assumption. apply <- lang_leq. intros w [j Hw]. setoid_rewrite lang_leq in H. eauto. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(MxGraph) Coq(List)