Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Apply andI with Subq x0 (472ec.. x0), ∀ x1 . prim1 x1 x0exactly1of2 (prim1 ((λ x2 . 15418.. x2 (91630.. (4ae4a.. 4a7ef..))) x1) x0) (prim1 x1 x0) leaving 2 subgoals.
Let x1 of type ι be given.
Assume H1: prim1 x1 x0.
Apply unknownprop_0b5b61a66a1ed2eb843dbce5c5f6930c63a284fe5e33704d9f0cc564310ec40b with x0, 94f9e.. x0 (λ x2 . (λ x3 . 15418.. x3 (91630.. (4ae4a.. 4a7ef..))) x2), x1.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H1: prim1 x1 x0.
Apply exactly1of2_I2 with prim1 ((λ x2 . 15418.. x2 (91630.. (4ae4a.. 4a7ef..))) x1) x0, prim1 x1 x0 leaving 2 subgoals.
Assume H2: prim1 ((λ x2 . 15418.. x2 (91630.. (4ae4a.. 4a7ef..))) x1) 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 H2.
The subproof is completed by applying H1.