Let r be given.
Assume Hr: r ∈ R.
We will prove Romega_singleton_seq r ∈ Romega_tilde 0.
We prove the intermediate claim HdefT: Romega_tilde 0 = {f ∈ R_omega_space|∀i : set, i ∈ ω → 0 ∈ 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 ∈ ω → 0 ∈ i → apply_fun f0 i = 0)) to the current goal.
An exact proof term for the current goal is (Romega_singleton_seq_in_Romega_space r Hr).
Let i be given.
Assume Hi: i ∈ ω.
Assume H0i: 0 ∈ i.
We will prove apply_fun (Romega_singleton_seq r) i = 0.
We prove the intermediate claim Happ: 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).
rewrite the current goal using Happ (from left to right).
rewrite the current goal using (If_i_1 (0 ∈ i) 0 r H0i) (from left to right).
Use reflexivity.
∎