proposition: Lemma prod2_comp1: forall p:prod2, prod2_conv2 (prod2_conv1 p) = p.
proof: Proof. intros. extensionality i. now destruct i. Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)