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