Let i be given.

Assume HiO: i ∈ ω.

Set Xi to be the term const_space_family ω R R_standard_topology.

We prove the intermediate claim HXi: apply_fun Xi i = (R,R_standard_topology).

An exact proof term for the current goal is (const_space_family_apply ω R R_standard_topology i HiO).

We will prove (apply_fun Xi i) 0 = R.

rewrite the current goal using HXi (from left to right).

An exact proof term for the current goal is (tuple_2_0_eq R R_standard_topology).

∎