Let I, X and i be given.

Assume Hi: i ∈ I.

We will prove apply_fun (const_family I X) i = X.

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

∎