proposition: Lemma finite_intersections_len_S_choice {X : Type} (F : Family X) (n : nat) : exists f : {U : Ensemble X | In (finite_intersections_len F (S n)) U} -> {U : Ensemble X | In (finite_intersections_len F n) U} * {U : Ensemble X | In (finite_intersections_len F 1) U}, forall U, proj1_sig U = Intersection (proj1_sig (fst (f U))) (proj1_sig (snd (f U))).
proof: Proof. apply choice with (R := fun U : {U : Ensemble X | In (finite_intersections_len F (S n)) U} => fun y : {U : Ensemble X | In (finite_intersections_len F n) U} * {U : Ensemble X | In (finite_intersections_len F 1) U} => proj1_sig U = Intersection (proj1_sig (fst y)) (proj1_sig (snd y))). intros [? HU]. destruct (finite_intersections_len_S_exists HU) as [V [W [HV [HW ?]]]]. now exists (exist _ V HV, exist _ W HW). Qed.
imports: Coq(Program.Equality) Coq(Lia) Coq(ClassicalChoice) Ensembles EnsemblesImplicit Families FiniteTypes IndexedFamilies CountableTypes Proj1SigInjective Powerset_facts