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 H2:
PNoLe x0 x2 x1 x3.
Assume H3:
PNoLe x1 x3 x0 x2.
Let x4 of type ο be given.
Assume H4:
x0 = x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x4.
Apply andE with
x0 = x1,
PNoEq_ x0 x2 x3,
x4 leaving 2 subgoals.
Apply unknownprop_1a9abde3fe02db6eaaf9e31d6ce1b4dfe880600f86eeace1659f415737e4bdb6 with
x0,
x1,
x2,
x3 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 H3.
The subproof is completed by applying H4.