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 Hxin: 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 Hxin).
We prove the intermediate claim HfinDiff: finite (X ∖ X).
rewrite the current goal using Hdiff_empty (from left to right).
An exact proof term for the current goal is finite_Empty.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) X (Self_In_Power X) (orIL (finite (X ∖ X)) (X = Empty) HfinDiff)).
∎