We will prove topology_on unit_interval I_topology.

An exact proof term for the current goal is unit_interval_topology_on.

∎