Let n, f and i be given.

Assume Hi: i ∈ ω.

We prove the intermediate claim Hdef: euclidean_space_extend_to_Romega n f = graph ω (λj : set ⇒ If_i (j ∈ n) (apply_fun f j) 0).

Use reflexivity.

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

An exact proof term for the current goal is (apply_fun_graph ω (λj : set ⇒ If_i (j ∈ n) (apply_fun f j) 0) i Hi).

∎