Search for blocks/addresses/...

Proofgold Proof

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