Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Let x2 of type ι → ο be given.
Apply unknownprop_d3eaeaf2c92929364f7d313ca2b01dbaa8e7169d84112bc61a6ed9c6cb0d624a with
λ x3 x4 : ι → (ι → ο) → (ι → ο) → ο . x4 x0 x1 x2 ⟶ ∀ x5 : ο . (∀ x6 . In x6 x0 ⟶ PNoEq_ x6 x1 x2 ⟶ not (x1 x6) ⟶ x2 x6 ⟶ x5) ⟶ x5.
Assume H0:
(λ x3 . λ x4 x5 : ι → ο . ∃ x6 . and (In x6 x3) (and (and (PNoEq_ x6 x4 x5) (not (x4 x6))) (x5 x6))) x0 x1 x2.
Let x3 of type ο be given.
Assume H1:
∀ x4 . In x4 x0 ⟶ PNoEq_ x4 x1 x2 ⟶ not (x1 x4) ⟶ x2 x4 ⟶ x3.
Apply H0 with
x3.
Let x4 of type ι be given.
Apply andE with
In x4 x0,
and (and (PNoEq_ x4 x1 x2) (not (x1 x4))) (x2 x4),
x3 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_1eb28f5831a9d21e218b89c238edbbf849d22045bb77ce7cec926a651d1793f0 with
PNoEq_ x4 x1 x2,
not (x1 x4),
x2 x4,
x3 leaving 2 subgoals.
The subproof is completed by applying H4.
Assume H7: x2 x4.
Apply H1 with
x4 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
The subproof is completed by applying H7.