Search for blocks/addresses/...

Proofgold Proof

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