Let I, X, Tx and i be given.

Assume Hi: i ∈ I.

We will prove apply_fun (const_space_family I X Tx) i = (X,Tx).

An exact proof term for the current goal is (const_fun_apply I (X,Tx) i Hi).

∎