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 x0 (94f9e.. x1 (λ x2 . (λ x3 . 15418.. x3 (91630.. (4ae4a.. 4a7ef..))) x2)).
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with x1, λ x2 . (λ x3 . 15418.. x3 (91630.. (4ae4a.. 4a7ef..))) x2, x0, False leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: prim1 x2 x1.
Assume H3: x0 = (λ x3 . 15418.. x3 (91630.. (4ae4a.. 4a7ef..))) x2.
Apply unknownprop_81d5bf525fa56ced1f50f507419c213d2f5baf8a9bd690d88066a9046e094314 with x2.
Apply H3 with λ x3 x4 . ordinal x3.
The subproof is completed by applying H0.