Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ο be given.
Let x3 of type ι → ο be given.
Assume H0:
PNoLt x0 x2 x1 x3.
Apply unknownprop_9c4323d14785b84a66d449068a5854b52f7f14bc003d3f63275870fa29b9e25d with
λ x4 x5 : ι → (ι → ο) → ι → (ι → ο) → ο . x5 x0 x2 x1 x3.
Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with
PNoLt x0 x2 x1 x3,
and (x0 = x1) (PNoEq_ x0 x2 x3).
The subproof is completed by applying H0.