Let r and i be given.
Assume Hr: r ∈ R.
Assume Hi: i ∈ ω.
We will prove apply_fun (Romega_singleton_seq r) i = If_i (0 ∈ i) 0 r.
We prove the intermediate claim Hdef: Romega_singleton_seq r = graph ω (λj : set ⇒ If_i (0 ∈ j) 0 r).
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 (0 ∈ j) 0 r) i Hi).
∎