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 H1:
PNoEq_ x0 x1 (λ x4 . or (x1 x4) (x4 = x0)).
Assume H2: x3 ∈ x0.
Assume H3:
PNoEq_ x3 (λ x4 . or (x1 x4) (x4 = x0)) x2.
Assume H5:
PNoLt x3 x2 x0 x1.
Assume H6:
PNoLt x0 x1 x3 x2.
Apply PNoLt_irref with
x0,
x1.
Apply PNoLt_tra with
x0,
x3,
x0,
x1,
x2,
x1 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
The subproof is completed by applying H0.
The subproof is completed by applying H6.
The subproof is completed by applying H5.