Let k and p be given.

Assume HkO: k ∈ ω.

Assume Hp: p ∈ setprod (Romega_tilde k) R.

We will prove apply_fun (Romega_extend_map k) p = Romega_extend_seq k p.

We prove the intermediate claim Hdef: Romega_extend_map k = graph (setprod (Romega_tilde k) R) (λq : set ⇒ Romega_extend_seq k q).

Use reflexivity.

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

An exact proof term for the current goal is (apply_fun_graph (setprod (Romega_tilde k) R) (λq : set ⇒ Romega_extend_seq k q) p Hp).

∎