Let I, X, Tx and i be given.
Assume Hi: i ∈ I.
We will prove space_family_topology (const_space_family I X Tx) i = Tx.
We prove the intermediate claim Hsf: space_family_topology (const_space_family I X Tx) i = (apply_fun (const_space_family I X Tx) i) 1.
Use reflexivity.
rewrite the current goal using Hsf (from left to right).
rewrite the current goal using (const_space_family_apply I X Tx i Hi) (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq X Tx).
∎