Let X and T be given.
Assume HT.
We prove the intermediate claim Hempty: Empty ∈ T.
An exact proof term for the current goal is (topology_has_empty X T HT).
We prove the intermediate claim HX: X ∈ T.
An exact proof term for the current goal is (topology_has_X X T HT).
Let U be given.
Assume HU: U ∈ indiscrete_topology X.
Apply UPairE U Empty X HU to the current goal.
Assume HUempty: U = Empty.
rewrite the current goal using HUempty (from left to right).
An exact proof term for the current goal is Hempty.
Assume HUX: U = X.
rewrite the current goal using HUX (from left to right).
An exact proof term for the current goal is HX.
∎