proposition: Lemma family_union_add {X : Type} (F : Family X) (U : Ensemble X) : FamilyUnion (Add F U) = Union (FamilyUnion F) U.
proof: Proof. apply Extensionality_Ensembles; split; red. - intros x Hx. destruct Hx as [A x HA Hx]. destruct HA as [A HA|A HA]. + left. exists A; auto. + destruct HA. right. assumption. - intros x Hx. destruct Hx as [x Hx|x Hx]. + destruct Hx as [A x HA Hx]. exists A; auto. left; auto. + exists U; auto. right. constructor. Qed.
imports: Coq(Classical_Prop) Coq(Classical_sets) Coq(Morphisms) ZornsLemma(Image ImageImplicit) ZornsLemma(EnsemblesImplicit)