Let g be given.
Assume H1.
Apply H1 to the current goal.
Assume H1: ∀n ∈ ω, g n ∈ 𝒫 ω.
Assume H2: ∀X ∈ 𝒫 ω, ∃n ∈ ω, g n = X.
Set D to be the term {n ∈ ω|n ∉ g n}.
We prove the intermediate claim L1: D ∈ 𝒫 ω.
Apply PowerI to the current goal.
Let n be given.
Assume Hn: n ∈ D.
We will prove n ∈ ω.
An exact proof term for the current goal is SepE1 ω (λn ⇒ n ∉ g n) n Hn.
Apply H2 D L1 to the current goal.
Let n be given.
Assume H3.
Apply H3 to the current goal.
Assume H3: n ∈ ω.
Assume H4: g n = D.
We prove the intermediate claim L2: n ∉ D.
Assume H5: n ∈ D.
Apply SepE2 ω (λn ⇒ n ∉ g n) n H5 to the current goal.
We will prove n ∈ g n.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is H5.
Apply L2 to the current goal.
We will prove n ∈ D.
Apply SepI to the current goal.
An exact proof term for the current goal is H3.
We will prove n ∉ g n.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is L2.
∎