proposition: Lemma IndexedIntersection_surj_fn {X A B : Type} (V : IndexedFamily A X) (f : B -> A) : surjective f -> IndexedIntersection V = IndexedIntersection (fun x => V (f x)).
proof: Proof. intros. apply Extensionality_Ensembles; split; red; intros. - destruct H0. constructor. intros. apply H0. - destruct H0. constructor. intros. destruct (H a). subst. apply H0. Qed.
imports: ZornsLemma(EnsemblesImplicit FunctionProperties)