We will prove topology_on long_line long_line_topology.

We prove the intermediate claim Hex: ∃T : set, topology_on long_line T.

We use (discrete_topology long_line) to witness the existential quantifier.

An exact proof term for the current goal is (discrete_topology_on long_line).

An exact proof term for the current goal is (Eps_i_ex (λT : set ⇒ topology_on long_line T) Hex).

∎