Let k and p be given.
Assume HkO: k ∈ ω.
Assume Hp: p ∈ setprod (Romega_tilde k) R.
We will prove Romega_extend_seq k p ∈ Romega_tilde (ordsucc k).
Set h to be the term (λi : set ⇒ 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 ω h.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
We prove the intermediate claim HdefT: Romega_tilde (ordsucc k) = {f ∈ R_omega_space|∀i : set, i ∈ ω → ordsucc k ∈ i → apply_fun f i = 0}.
Use reflexivity.
rewrite the current goal using HdefT (from left to right).
Apply (SepI R_omega_space (λf0 : set ⇒ ∀i : set, i ∈ ω → ordsucc k ∈ i → apply_fun f0 i = 0)) to the current goal.
Apply (graph_omega_in_Romega_space h) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
We will prove h i ∈ R.
We prove the intermediate claim Hhi: h i = If_i (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)).
Use reflexivity.
rewrite the current goal using Hhi (from left to right).
Apply (xm (ordsucc k ∈ i)) to the current goal.
Assume Hki: ordsucc k ∈ i.
rewrite the current goal using (If_i_1 (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)) Hki) (from left to right).
An exact proof term for the current goal is real_0.
Assume Hnki: ¬ (ordsucc k ∈ i).
rewrite the current goal using (If_i_0 (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)) Hnki) (from left to right).
Apply (xm (i = ordsucc k)) to the current goal.
Assume Hieq.
rewrite the current goal using (If_i_1 (i = ordsucc k) (p 1) (apply_fun (p 0) i) Hieq) (from left to right).
We prove the intermediate claim Hp1: p 1 ∈ R.
We prove the intermediate claim Hp1raw: p 1 ∈ (λ_ : set ⇒ R) (p 0).
An exact proof term for the current goal is (ap1_Sigma (Romega_tilde k) (λ_ : set ⇒ R) p Hp).
An exact proof term for the current goal is Hp1raw.
An exact proof term for the current goal is Hp1.
Assume Hineq.
rewrite the current goal using (If_i_0 (i = ordsucc k) (p 1) (apply_fun (p 0) i) Hineq) (from left to right).
We prove the intermediate claim Hp0: p 0 ∈ Romega_tilde k.
An exact proof term for the current goal is (ap0_Sigma (Romega_tilde k) (λ_ : set ⇒ R) p Hp).
We prove the intermediate claim Hp0X: p 0 ∈ R_omega_space.
An exact proof term for the current goal is (Romega_tilde_sub_Romega k (p 0) Hp0).
An exact proof term for the current goal is (Romega_coord_in_R (p 0) i Hp0X Hi).
Let i be given.
Assume Hi: i ∈ ω.
Assume Hki: ordsucc k ∈ i.
We will prove apply_fun (graph ω h) i = 0.
We prove the intermediate claim Happ: apply_fun (graph ω h) i = h i.
An exact proof term for the current goal is (apply_fun_graph ω h i Hi).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hhi: h i = If_i (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)).
Use reflexivity.
rewrite the current goal using Hhi (from left to right).
rewrite the current goal using (If_i_1 (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)) Hki) (from left to right).
Use reflexivity.
∎