Let X and T be given.
Assume HT.
We will prove topology_on X T ∧ topology_on X T ∧ T = T.
Apply and3I to the current goal.
An exact proof term for the current goal is HT.
An exact proof term for the current goal is HT.
Use reflexivity.
∎