Assume H1: equip ω (𝒫 ω).

Apply H1 to the current goal.

Let g be given.

Assume H2: bij ω (𝒫 ω) g.

Apply form100_22_v3 g to the current goal.

We will prove surj ω (𝒫 ω) g.

Apply bij_surj to the current goal.

An exact proof term for the current goal is H2.

∎