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:
PNoLe x0 x3 x1 x4.
Assume H4:
PNoLt x1 x4 x2 x5.
Apply unknownprop_a0b9870a33f18f7eb5aaf7ae107d529d6499166437a3535589b34653050e816a with
x0,
x1,
x3,
x4,
PNoLt x0 x3 x2 x5 leaving 3 subgoals.
The subproof is completed by applying H3.
Assume H5:
PNoLt x0 x3 x1 x4.
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 H5.
The subproof is completed by applying H4.
Assume H5: x0 = x1.
Apply H5 with
λ x6 x7 . PNoLt x7 x3 x2 x5.
Apply unknownprop_48a8f82c26b065656db6bac0064b1ef0047f4abc8104b10440bc49b824b6ee3c with
x1,
x2,
x3,
x4,
x5 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply H5 with
λ x6 x7 . PNoEq_ x6 x3 x4.
The subproof is completed by applying H6.
The subproof is completed by applying H4.