Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: atleastp (prim4 x0) x0. Apply H0 with False. Let x1 of type ι → ι be given. Assume H1: inj (prim4 x0) x0 x1. Apply form100_63_Cantor with x0, x1. The subproof is completed by applying H1. ■