Assume Hcases: U = Empty ∨ U = X.

We prove the intermediate claim HUempty_branch: U = Empty → U ∈ indiscrete_topology X.

Assume HUE: U = Empty.

rewrite the current goal using HUE (from left to right).

An exact proof term for the current goal is (UPairI1 Empty X).

We prove the intermediate claim HUx_branch: U = X → U ∈ indiscrete_topology X.

Assume HUX: U = X.

rewrite the current goal using HUX (from left to right).

An exact proof term for the current goal is (UPairI2 Empty X).

An exact proof term for the current goal is (Hcases (U ∈ indiscrete_topology X) HUempty_branch HUx_branch).