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