Let X be given.
Assume HinfX: infinite X.
We will prove ∃U V : set, U ∈ infinite_complement_family X ∧ V ∈ infinite_complement_family X.
We use Empty to witness the existential quantifier.
We use X to witness the existential quantifier.
Apply andI to the current goal.
We will prove Empty ∈ infinite_complement_family X.
We prove the intermediate claim Hdisj: infinite (X ∖ Empty) ∨ Empty = Empty ∨ Empty = X.
Apply orIL to the current goal.
Apply orIR to the current goal.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ infinite (X ∖ U0) ∨ U0 = Empty ∨ U0 = X) Empty (Empty_In_Power X) Hdisj).
We will prove X ∈ infinite_complement_family X.
We prove the intermediate claim Hdisj: infinite (X ∖ X) ∨ X = Empty ∨ X = X.
Apply orIR to the current goal.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ infinite (X ∖ U0) ∨ U0 = Empty ∨ U0 = X) X (Self_In_Power X) Hdisj).
∎