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