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: or (40dde.. x0 x3 x1 x4) (and (x0 = x1) (PNoEq_ x0 x3 x4)).
Assume H4: 40dde.. x1 x4 x2 x5.
Apply H3 with 40dde.. x0 x3 x2 x5 leaving 2 subgoals.
Assume H5: 40dde.. x0 x3 x1 x4.
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 H5.
The subproof is completed by applying H4.
Assume H5: and (x0 = x1) (PNoEq_ x0 x3 x4).
Apply H5 with 40dde.. x0 x3 x2 x5.
Assume H6: x0 = x1.
Assume H7: PNoEq_ x0 x3 x4.
Apply H6 with λ x6 x7 . 40dde.. x7 x3 x2 x5.
Apply unknownprop_516ec77a0547bdde87f302357c77a8c500e4737d03bed523bd783f1c87c1572b with x1, x2, x3, x4, x5 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply H6 with λ x6 x7 . PNoEq_ x6 x3 x4.
The subproof is completed by applying H7.
The subproof is completed by applying H4.
■