Apply H1 with
λ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) x2 = TwoRamseyGraph_3_5_Church13 x2 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) leaving 13 subgoals.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H2:
x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)).
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H2:
x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x4)) (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x4) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)).
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H2:
x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x5)) (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x5) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)).
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H2:
x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x6)) (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x6) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)).
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H2:
x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x7)) (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x7) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)).
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H2:
x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x8)) (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x8) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)).
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H2:
x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x9)) (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x9) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)).
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H2:
x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x10)) (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x10) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)).
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H2:
x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x11)) (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x11) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)).
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H2:
x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x12)) (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x12) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)).
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H2:
x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x13)) (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x13) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)).
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H2:
x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x14)) (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x14) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)).
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H2:
x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x15)) (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x15) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)).
The subproof is completed by applying H2.