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.
Apply H2 with
or (PNoLt x0 x2 x1 x4) (and (x0 = x1) (PNoEq_ x0 x2 x4)) leaving 2 subgoals.
Assume H4:
PNoLt x0 x2 x1 x3.
Apply orIL with
PNoLt x0 x2 x1 x4,
and (x0 = x1) (PNoEq_ x0 x2 x4).
Apply PNoLtEq_tra 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.
Apply H4 with
or (PNoLt x0 x2 x1 x4) (and (x0 = x1) (PNoEq_ x0 x2 x4)).
Assume H5: x0 = x1.
Apply orIR with
PNoLt x0 x2 x1 x4,
and (x0 = x1) (PNoEq_ x0 x2 x4).
Apply andI with
x0 = x1,
PNoEq_ x0 x2 x4 leaving 2 subgoals.
The subproof is completed by applying H5.
Apply PNoEq_tra_ with
x0,
x2,
x3,
x4 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply H5 with
λ x5 x6 . PNoEq_ x6 x3 x4.
The subproof is completed by applying H3.