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.
Let x5 of type ι → ο be given.
Assume H3:
PNoLt x0 x3 x1 x4.
Assume H4:
PNoLe x1 x4 x2 x5.
Apply unknownprop_a0b9870a33f18f7eb5aaf7ae107d529d6499166437a3535589b34653050e816a with
x1,
x2,
x4,
x5,
PNoLt x0 x3 x2 x5 leaving 3 subgoals.
The subproof is completed by applying H4.
Assume H5:
PNoLt x1 x4 x2 x5.
Apply unknownprop_6bb26b25b4b138d2d5816191bcd658afb4958cf8c28d95f1e213b943c7319173 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: x1 = x2.
Apply H5 with
λ x6 x7 . PNoLt x0 x3 x6 x5.
Apply unknownprop_0661190d7cd643d10a13ae09e94eb6be9e80fd8af7f023e17f840b06a894f274 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 H6.