Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply H0 with
TwoRamseyProp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x3.
Let x4 of type ι → ι be given.
Apply H1 with
TwoRamseyProp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x3.
Assume H2: ∀ x5 . x5 ∈ x2 ⟶ x4 x5 ∈ x3.
Assume H3: ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6.
Let x5 of type ι → ι → ο be given.
Assume H5: ∀ x6 x7 . x5 x6 x7 ⟶ x5 x7 x6.
Apply H4 with
λ x6 x7 . x5 (x4 x6) (x4 x7),
or (∃ x6 . and (x6 ⊆ x3) (and (equip x0 x6) (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ x5 x7 x8))) (∃ x6 . and (x6 ⊆ x3) (and (equip x1 x6) (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ not (x5 x7 x8)))) leaving 3 subgoals.
The subproof is completed by applying L6.
Assume H7:
∃ x6 . and (x6 ⊆ x2) (and (equip x0 x6) (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ x5 (x4 x7) (x4 x8))).
Apply H7 with
or (∃ x6 . and (x6 ⊆ x3) (and (equip x0 x6) (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ x5 x7 x8))) (∃ x6 . and (x6 ⊆ x3) (and (equip x1 x6) (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ not (x5 x7 x8)))).
Let x6 of type ι be given.
Assume H8:
(λ x7 . and (x7 ⊆ x2) (and (equip x0 x7) (∀ x8 . x8 ∈ x7 ⟶ ∀ x9 . x9 ∈ x7 ⟶ (x8 = x9 ⟶ ∀ x10 : ο . x10) ⟶ x5 (x4 x8) (x4 x9)))) x6.
Apply H8 with
or (∃ x7 . and (x7 ⊆ x3) (and (equip x0 x7) (∀ x8 . x8 ∈ x7 ⟶ ∀ x9 . x9 ∈ x7 ⟶ (x8 = x9 ⟶ ∀ x10 : ο . x10) ⟶ x5 x8 x9))) (∃ x7 . and (x7 ⊆ x3) (and (equip x1 x7) (∀ x8 . ... ⟶ ∀ x9 . ... ⟶ ... ⟶ not ...))).