Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_1019f796b5519c5beeeef55b1daae2de48848a97e75d217687db0a2449fd5208.
set y2 to be λ x2 x3 . x3
set y3 to be λ x3 x4 . x3
Claim L3: ∀ x4 : (ι → ι → ι) → ο . x4 y3 ⟶ x4 y2
Let x4 of type (ι → ι → ι) → ο be given.
Assume H3: x4 (λ x5 x6 . x5).
set y5 to be λ x5 : ι → ι → ι . x4
Apply unknownprop_d1ab6c05d827ab2f0497648eeb2e74b0b0260f4e004a74cbc06a5c0a175e4a2a with
λ x6 x7 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple y2) (nth_6_tuple y3) x7 x7 = λ x8 x9 . x9,
λ x6 x7 : ι → ι → ι . y5 x7 x6 leaving 2 subgoals.
Apply unknownprop_8cd4991a6104c55e6eccf931d2bcd091b5ab0b7c97b971c3abc9b786d20cbd4d with
nth_6_tuple y2,
nth_6_tuple y3 leaving 2 subgoals.
Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with
y2.
The subproof is completed by applying H0.
Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with
y3.
The subproof is completed by applying H1.
Apply H2 with
λ x6 : ι → ι → ι . y5 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying In_5_6.
The subproof is completed by applying In_5_6.
The subproof is completed by applying H3.
Let x4 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Apply L3 with
λ x5 : ι → ι → ι . x4 x5 y3 ⟶ x4 y3 x5.
Assume H4: x4 y3 y3.
The subproof is completed by applying H4.