Proofgold Proof

pf
Assume H0: equip omega (prim4 omega). Apply H0 with False. Let x0 of type ι → ι be given. Assume H1: bij omega (prim4 omega) x0. Apply form100_22_v3 with x0. Apply bij_surj with omega, prim4 omega, x0. The subproof is completed by applying H1. ■