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

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

Assume H1: ∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3).

Assume H2: ∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3)).

Let x1 of type ι be given.

Assume H3: x1 ∈ u18.

Apply unknownprop_45d11dce2d0b092bd17c01d64c29c5885c90b43dc7cb762c6d6ada999ea508c5 with u13, setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1)), atleastp (setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))) u13 leaving 3 subgoals.

The subproof is completed by applying nat_13.

The subproof is completed by applying H4.

Claim L5: ...

...

Apply L5 with x0, atleastp (setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))) u13 leaving 3 subgoals.

The subproof is completed by applying H0.

Assume H6: ∃ x2 . and (x2 ⊆ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))) (and (equip u3 x2) (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x0 x3 x4)).

Apply H6 with False.

Let x2 of type ι be given.

Assume H7: (λ x3 . and (x3 ⊆ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))) (and (equip u3 x3) (∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ x0 x4 x5))) x2.

Apply H7 with False.

Assume H9: and (equip u3 x2) (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x0 x3 x4).

Apply H9 with False.

Assume H10: equip u3 x2.

Assume H11: ∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x0 x3 x4.

Apply H1 with x2 leaving 3 subgoals.

Apply Subq_tra with x2, setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) ...), ... leaving 2 subgoals.

...

■

Proofgold Proof