proposition: Lemma IndexedIntersection_option_Intersection {X A : Type} (V : IndexedFamily (option X) A) : IndexedIntersection V = Intersection (IndexedIntersection (fun a => V (Some a))) (V None).
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - destruct H. constructor. + constructor. intros. apply H. + apply H. - destruct H. destruct H. constructor. intros. destruct a; auto. Qed.
imports: ZornsLemma(EnsemblesImplicit FunctionProperties)