Let k, p and i be given.
Assume Hi: i ∈ ω.
We will prove apply_fun (Romega_extend_seq k p) i = If_i (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)).
We prove the intermediate claim Hdef: Romega_extend_seq k p = graph ω (λj : set ⇒ If_i (ordsucc k ∈ j) 0 (If_i (j = ordsucc k) (p 1) (apply_fun (p 0) j))).
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 (ordsucc k ∈ j) 0 (If_i (j = ordsucc k) (p 1) (apply_fun (p 0) j))) i Hi).
∎