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 H0: ∀ x4 . In x4 x0 ⟶ PNoEq_ x4 x1 x2 ⟶ not (x1 x4) ⟶ x2 x4 ⟶ x3.

Apply unknownprop_d3eaeaf2c92929364f7d313ca2b01dbaa8e7169d84112bc61a6ed9c6cb0d624a with λ x4 x5 : ι → (ι → ο) → (ι → ο) → ο . x5 x0 x1 x2 ⟶ x3.

Assume H1: (λ x4 . λ x5 x6 : ι → ο . ∃ x7 . and (In x7 x4) (and (and (PNoEq_ x7 x5 x6) (not (x5 x7))) (x6 x7))) x0 x1 x2.

Apply H1 with x3.

Let x4 of type ι be given.

Assume H2: (λ x5 . and (In x5 x0) (and (and (PNoEq_ x5 x1 x2) (not (x1 x5))) (x2 x5))) x4.

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.

Assume H3: In x4 x0.

Assume H4: and (and (PNoEq_ x4 x1 x2) (not (x1 x4))) (x2 x4).

Apply unknownprop_1eb28f5831a9d21e218b89c238edbbf849d22045bb77ce7cec926a651d1793f0 with PNoEq_ x4 x1 x2, not (x1 x4), x2 x4, x3 leaving 2 subgoals.

The subproof is completed by applying H4.

Apply H0 with x4.

The subproof is completed by applying H3.

■

Proofgold Proof