Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι be given.
Assume H0: ordinal x1.
Let x2 of type ι → ο be given.
Let x3 of type ι → ο be given.
Assume H1: PNoEq_ x1 x2 x3.
Assume H2: cae4c.. x0 x1 x2.
Let x4 of type ι be given.
Assume H3: ordinal x4.
Let x5 of type ι → ο be given.
Assume H4: x0 x4 x5.
Apply unknownprop_8400f668ce579075dd52a6b0bc8eaa2c816f68129d64497b65439b55d60266f7 with x4, x1, x5, x2, x3 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H0.
Apply H2 with x4, x5 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H1.
■