Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: ordinal x0.
Assume H1: ordinal x1.
Assume H2: ordinal x2.
Let x3 of type ι → ο be given.
Let x4 of type ι → ο be given.
Let x5 of type ι → ο be given.
Assume H3: 40dde.. x0 x3 x1 x4.
Assume H4: or (40dde.. x1 x4 x2 x5) (and (x1 = x2) (PNoEq_ x1 x4 x5)).
Apply H4 with 40dde.. x0 x3 x2 x5 leaving 2 subgoals.
Assume H5: 40dde.. x1 x4 x2 x5.
Apply unknownprop_37f5b5c6ee0011f262b499567d54413188e5bd83bd5555e5f3caca08d2fd472f with x0, x1, x2, x3, x4, x5 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
Assume H5: and (x1 = x2) (PNoEq_ x1 x4 x5).
Apply H5 with 40dde.. x0 x3 x2 x5.
Assume H6: x1 = x2.
Assume H7: PNoEq_ x1 x4 x5.
Apply H6 with λ x6 x7 . 40dde.. x0 x3 x6 x5.
Apply unknownprop_8400f668ce579075dd52a6b0bc8eaa2c816f68129d64497b65439b55d60266f7 with x0, x1, x3, x4, x5 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H7.
■