Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Let x1 of type ι → ι → ι → ι → ι → ι → ι be given.
Apply H0 with
λ x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a x2 x1 (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8) = λ x3 x4 . x3 leaving 6 subgoals.
Apply H1 with
λ x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a (λ x3 x4 x5 x6 x7 x8 . x3) x2 (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8) = λ x3 x4 . x3 leaving 6 subgoals.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
The subproof is completed by applying H2.
Apply H1 with
λ x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a (λ x3 x4 x5 x6 x7 x8 . x4) x2 (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8) = λ x3 x4 . x3 leaving 6 subgoals.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
The subproof is completed by applying H2.
Apply H1 with
λ x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a (λ x3 x4 x5 x6 x7 x8 . x5) x2 (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8) = λ x3 x4 . x3 leaving 6 subgoals.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
The subproof is completed by applying H2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.