Let n be given.
Assume HnO: n ∈ ω.
We will prove Romega_zero ∈ Romega_tilde n.
We prove the intermediate claim Hbase: Romega_zero ∈ R_omega_space.
An exact proof term for the current goal is Romega_zero_in_Romega_space.
We prove the intermediate claim Hprop: ∀i : set, i ∈ ω → n ∈ i → apply_fun Romega_zero i = 0.
Let i be given.
Assume Hi: i ∈ ω.
Assume Hni: n ∈ i.
We will prove apply_fun Romega_zero i = 0.
An exact proof term for the current goal is (const_fun_apply ω 0 i Hi).
An exact proof term for the current goal is (SepI R_omega_space (λf0 : set ⇒ ∀i : set, i ∈ ω → n ∈ i → apply_fun f0 i = 0) Romega_zero Hbase Hprop).
∎