Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Let x1 of type ι → ο be given.
Let x2 of type ι be given.
Assume H1: ordinal x2.
Let x3 of type ι → ο be given.
Assume H2: 7eb85.. x0 x1 x2 x3.
Let x4 of type ι be given.
Assume H3: ordinal x4.
Let x5 of type ι → ο be given.
Assume H4: 0dfb2.. x0 x1 x4 x5.
Apply H2 with 40dde.. x2 x3 x4 x5.
Assume H5: prim1 x2 x0.
Assume H6: 40dde.. x2 x3 x0 x1.
Apply H4 with 40dde.. x2 x3 x4 x5.
Assume H7: prim1 x4 x0.
Assume H8: 40dde.. x0 x1 x4 x5.
Apply unknownprop_37f5b5c6ee0011f262b499567d54413188e5bd83bd5555e5f3caca08d2fd472f with x2, x0, x4, x3, x1, x5 leaving 5 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
■