Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: ordinal x0.
Assume H1: prim1 (15418.. x1 (91630.. (4ae4a.. 4a7ef..))) x0.
Apply unknownprop_81d5bf525fa56ced1f50f507419c213d2f5baf8a9bd690d88066a9046e094314 with x1.
Apply ordinal_Hered with x0, (λ x2 . 15418.. x2 (91630.. (4ae4a.. 4a7ef..))) x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
■