Let X and U be given.
Assume HU: U ∈ countable_complement_topology X.
Assume Hnemp: U ≠ Empty.
We will prove countable (X ∖ U).
We prove the intermediate claim Hprop: countable (X ∖ U) ∨ U = Empty.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λV : set ⇒ countable (X ∖ V) ∨ V = Empty) U HU).
We prove the intermediate claim Hcount_branch: countable (X ∖ U) → countable (X ∖ U).
Assume Hcount.
An exact proof term for the current goal is Hcount.
We prove the intermediate claim Hempty_branch: U = Empty → countable (X ∖ U).
Assume HUeq.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnemp HUeq).
An exact proof term for the current goal is (Hprop (countable (X ∖ U)) Hcount_branch Hempty_branch).
∎