proposition: Lemma family_union_union {X : Type} (F G : Family X) : FamilyUnion (Union F G) = Union (FamilyUnion F) (FamilyUnion G).
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - inversion H; subst; clear H. destruct H0; [left|right]; exists x0; auto. - destruct H, H; exists S; auto; [left|right]; auto. Qed.
imports: Coq(Classical_Prop) Coq(Classical_sets) Coq(Morphisms) ZornsLemma(Image ImageImplicit) ZornsLemma(EnsemblesImplicit)