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:
∀ x4 . x4 ∈ x0 ⟶ PNoEq_ x4 x1 x2 ⟶ not (x1 x4) ⟶ x2 x4 ⟶ x3.
Apply H0 with
x3.
Let x4 of type ι be given.
Assume H2:
(λ x5 . and (x5 ∈ x0) (and (and (PNoEq_ x5 x1 x2) (not (x1 x5))) (x2 x5))) x4.
Apply H2 with
x3.
Assume H3: x4 ∈ x0.
Apply H4 with
x3.
Apply H5 with
x2 x4 ⟶ x3.
Assume H8: x2 x4.
Apply H1 with
x4 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H8.