Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: 80242.. x0. Apply unknownprop_2c27682abc32e1c8a2160a07043a81afe1f256df4f0472edf3cf11efdcea8609 with x0, 1beb9.. (e4431.. x0) x0 leaving 2 subgoals. The subproof is completed by applying H0. Assume H1: ordinal (e4431.. x0). Assume H2: 1beb9.. (e4431.. x0) x0. The subproof is completed by applying H2. ■