Let x0 of type ι be given.

Let x1 of type ι → ο be given.

Apply unknownprop_d3eaeaf2c92929364f7d313ca2b01dbaa8e7169d84112bc61a6ed9c6cb0d624a with λ x2 x3 : ι → (ι → ο) → (ι → ο) → ο . not (x3 x0 x1 x1).

Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with (λ x2 . λ x3 x4 : ι → ο . ∃ x5 . and (In x5 x2) (and (and (PNoEq_ x5 x3 x4) (not (x3 x5))) (x4 x5))) x0 x1 x1.

Assume H0: (λ x2 . λ x3 x4 : ι → ο . ∃ x5 . and (In x5 x2) (and (and (PNoEq_ x5 x3 x4) (not (x3 x5))) (x4 x5))) x0 x1 x1.

Apply H0 with False.

Let x2 of type ι be given.

Assume H1: (λ x3 . and (In x3 x0) (and (and (PNoEq_ x3 x1 x1) (not (x1 x3))) (x1 x3))) x2.

Apply andE with In x2 x0, and (and (PNoEq_ x2 x1 x1) (not (x1 x2))) (x1 x2), False leaving 2 subgoals.

The subproof is completed by applying H1.

Assume H2: In x2 x0.

Assume H3: and (and (PNoEq_ x2 x1 x1) (not (x1 x2))) (x1 x2).

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

The subproof is completed by applying H3.

Assume H4: PNoEq_ x2 x1 x1.

Assume H5: not (x1 x2).

Assume H6: x1 x2.

Apply notE with x1 x2 leaving 2 subgoals.

The subproof is completed by applying H5.

The subproof is completed by applying H6.

■

Proofgold Proof