An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) Empty (Empty_In_Power X) (orIR (finite (X ∖ Empty)) (Empty = Empty) (λP H ⇒ H))).