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