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:
PNoLt x0 x2 x1 x3 ⟶ x4.
Assume H3:
x0 = x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x4.
Assume H4:
PNoLt x1 x3 x0 x2 ⟶ x4.
Apply unknownprop_ca18603a3bd7d3baee9f63f87aac7064ee948e21e70ee2e74fd135602574a894 with
PNoLt x0 x2 x1 x3,
and (x0 = x1) (PNoEq_ x0 x2 x3),
PNoLt x1 x3 x0 x2,
x4 leaving 4 subgoals.
Apply unknownprop_0f2b5ecd23fc753ac25b20b66aca31b1ee2798d140a64b03f95e3a4afaa4603d with
x0,
x1,
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply andE with
x0 = x1,
PNoEq_ x0 x2 x3,
x4 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H3.
The subproof is completed by applying H4.