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.
Let x3 of type ιο be given.
Let x4 of type ιο be given.
Assume H0: ordinal x1.
Assume H1: ordinal x2.
Apply unknownprop_10b092fb3ef85ea31ee360e7dc788511bcc4358b1df6c96ac348bc4af6827002 with x0, x1, x3, PNoLe x2 x4 x1 x3PNo_downc x0 x2 x4.
Let x5 of type ι be given.
Assume H2: ordinal x5.
Let x6 of type ιο be given.
Assume H3: x0 x5 x6.
Assume H4: PNoLe x1 x3 x5 x6.
Assume H5: PNoLe x2 x4 x1 x3.
Apply unknownprop_df2ff7ab23c8ea39e7f5ea4f6d5677729f8f4e104427ae8df8ddcc2119ec044a with x5, x6, x0, x2, x4 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_e94a13b4ac63cce4a867fc33d11c1ef6b397fe3905a6599da4996709c5166382 with x2, x1, x5, x4, x3, x6 leaving 5 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H5.
The subproof is completed by applying H4.