Let X be given.
We prove the intermediate claim Hdiff_empty: X ∖ X = Empty.
Apply Empty_Subq_eq to the current goal.
Let x be given.
Assume Hx.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X X x Hx).
We prove the intermediate claim Hxnot: x ∉ X.
An exact proof term for the current goal is (setminusE2 X X x Hx).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnot HxX).
We prove the intermediate claim HcountDiff: countable (X ∖ X).
rewrite the current goal using Hdiff_empty (from left to right).
An exact proof term for the current goal is (Subq_atleastp Empty ω (Subq_Empty ω)).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ countable (X ∖ U0) ∨ U0 = Empty) X (Self_In_Power X) (orIL (countable (X ∖ X)) (X = Empty) HcountDiff)).
∎