Let r be given.
Assume Hr: r ∈ R.
We will prove Romega_singleton_seq r ∈ R_omega_space.
We prove the intermediate claim Hdef: Romega_singleton_seq r = graph ω (λi : set ⇒ If_i (0 ∈ i) 0 r).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply (graph_omega_in_Romega_space (λi : set ⇒ If_i (0 ∈ i) 0 r)) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
We will prove If_i (0 ∈ i) 0 r ∈ R.
Apply (xm (0 ∈ i)) to the current goal.
Assume H0i: 0 ∈ i.
rewrite the current goal using (If_i_1 (0 ∈ i) 0 r H0i) (from left to right).
An exact proof term for the current goal is real_0.
Assume Hn0i: ¬ (0 ∈ i).
rewrite the current goal using (If_i_0 (0 ∈ i) 0 r Hn0i) (from left to right).
An exact proof term for the current goal is Hr.
∎