Let x0 of type ι → ι → ο be given.

Assume H0: ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1.

Assume H1: not (or (∃ x1 . and (x1 ⊆ u9) (and (equip u3 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3))) (∃ x1 . and (x1 ⊆ u9) (and (equip u4 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))))).

Let x1 of type ι be given.

Assume H2: x1 ∈ u9.

Let x2 of type ο be given.

Assume H3: ∀ x3 . x3 ∈ u9 ⟶ ∀ x4 . x4 ∈ u9 ⟶ ∀ x5 . x5 ∈ u9 ⟶ (x1 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ x0 x1 x3 ⟶ x0 x1 x4 ⟶ x0 x1 x5 ⟶ x2.

Apply dneg with x2.

Assume H4: not x2.

Claim L5: ...

...

Apply L5 with False.

Let x3 of type ι be given.

Assume H6: (λ x4 . and (x4 ⊆ u9) (and (and (atleastp u6 x4) (nIn x1 x4)) (∀ x5 . x5 ∈ u9 ⟶ x0 x1 x5 ⟶ nIn x5 x4))) x3.

Apply H6 with False.

Assume H7: x3 ⊆ u9.

Assume H8: and (and (atleastp u6 x3) (nIn x1 x3)) (∀ x4 . x4 ∈ u9 ⟶ x0 x1 x4 ⟶ nIn x4 x3).

Apply H8 with False.

Assume H9: and (atleastp u6 x3) (nIn x1 x3).

Apply H9 with (∀ x4 . x4 ∈ u9 ⟶ x0 x1 x4 ⟶ nIn x4 x3) ⟶ False.

Assume H10: atleastp u6 x3.

Assume H11: nIn x1 x3.

Assume H12: ∀ x4 . x4 ∈ u9 ⟶ x0 x1 x4 ⟶ nIn x4 x3.

Claim L13: ...

...

Apply L13 with x0, False leaving 3 subgoals.

The subproof is completed by applying H0.

Assume H14: ∃ x4 . and (x4 ⊆ x3) (and (equip u3 x4) (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ (x5 = x6 ⟶ ∀ x7 : ο . x7) ⟶ x0 x5 x6)).

Apply H14 with False.

Let x4 of type ι be given.

Assume H15: (λ x5 . and (x5 ⊆ x3) (and (equip u3 x5) (∀ x6 . x6 ∈ x5 ⟶ ∀ x7 . x7 ∈ x5 ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ x0 x6 x7))) x4.

Apply H15 with False.

Assume H16: x4 ⊆ ....

...

■

Proofgold Proof