Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: In x0 x1.

Let x2 of type ι → ο be given.

Let x3 of type ι → ο be given.

Assume H1: PNoEq_ x0 x2 x3.

Assume H2: not (x2 x0).

Assume H3: x3 x0.

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

Let x4 of type ο be given.

Assume H4: ∀ x5 . and (In x5 x1) (and (and (PNoEq_ x5 x2 x3) (not (x2 x5))) (x3 x5)) ⟶ x4.

Apply H4 with x0.

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

The subproof is completed by applying H0.

Apply unknownprop_c7bf67064987d41cefc55afb6af6ecbbb6b830405f2005e0def6e504b3ca3bf3 with PNoEq_ x0 x2 x3, not (x2 x0), x3 x0 leaving 3 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

The subproof is completed by applying H3.

■

Proofgold Proof