Let X, T1 and T2 be given.
Assume H.
We prove the intermediate claim Hpair: topology_on X T1 ∧ topology_on X T2.
An exact proof term for the current goal is (andEL (topology_on X T1 ∧ topology_on X T2) (T1 = T2) H).
We prove the intermediate claim Heq: T1 = T2.
An exact proof term for the current goal is (andER (topology_on X T1 ∧ topology_on X T2) (T1 = T2) H).
We prove the intermediate claim HT1: topology_on X T1.
An exact proof term for the current goal is (andEL (topology_on X T1) (topology_on X T2) Hpair).
We prove the intermediate claim HT2: topology_on X T2.
An exact proof term for the current goal is (andER (topology_on X T1) (topology_on X T2) Hpair).
We will prove topology_on X T2 ∧ topology_on X T1 ∧ T2 = T1.
Apply and3I to the current goal.
An exact proof term for the current goal is HT2.
An exact proof term for the current goal is HT1.
rewrite the current goal using Heq (from right to left).
Use reflexivity.
∎