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_10b092fb3ef85ea31ee360e7dc788511bcc4358b1df6c96ac348bc4af6827002 with
x0,
x1,
x3,
PNoLe x2 x4 x1 x3 ⟶ PNo_downc x0 x2 x4.
Let x5 of type ι be given.
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.