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 H3 with
λ x4 : ι → ι → ι → ι → ι → ι → ι . ((x0 = λ x5 x6 x7 x8 x9 x10 . x10) ⟶ (x1 = λ x5 x6 x7 x8 x9 x10 . x10) ⟶ False) ⟶ ((x4 = λ x5 x6 x7 x8 x9 x10 . x10) ⟶ (x3 = λ x5 x6 x7 x8 x9 x10 . x10) ⟶ False) ⟶ (x0 = x4 ⟶ x1 = x3 ⟶ False) ⟶ (TwoRamseyGraph_4_6_Church6_squared_a x0 x1 x4 x3 = λ x5 x6 . x5) ⟶ TwoRamseyGraph_4_6_Church6_squared_b x0 x1 x4 x3 = λ x5 x6 . x5 leaving 6 subgoals.
Assume H5:
(x0 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ False.
Assume H6:
((λ x4 x5 x6 x7 x8 x9 . x4) = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ (x3 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ False.
Assume H7:
(x0 = λ x4 x5 x6 x7 x8 x9 . x4) ⟶ x1 = x3 ⟶ False.
Apply unknownprop_c5c271fc2ac3b14d20f4a11b818283185c3ea9d0e453c95085ee5699f2cf2a6c with
x0,
x1,
λ x4 x5 x6 x7 x8 x9 . x4,
x3 leaving 6 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying unknownprop_b4d57e27d2e512a451dc25211a8e223b40ed9465fc8a3c8bd751dba0d369c058.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H7.
Assume H5:
(x0 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ False.
Assume H6:
((λ x4 x5 x6 x7 x8 x9 . x5) = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ (x3 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ False.
Assume H7:
(x0 = λ x4 x5 x6 x7 x8 x9 . x5) ⟶ x1 = x3 ⟶ False.
Apply unknownprop_c5c271fc2ac3b14d20f4a11b818283185c3ea9d0e453c95085ee5699f2cf2a6c with
x0,
x1,
λ x4 x5 x6 x7 x8 x9 . x5,
x3 leaving 6 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying unknownprop_f7c46973e8e993d589db2c7d2cbf123c412a9a004aa6a11277cf54d2a8c9b340.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H7.
Assume H5:
(x0 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ False.
Assume H6:
((λ x4 x5 x6 x7 x8 x9 . x6) = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ (x3 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ False.
Assume H7:
(x0 = λ x4 x5 x6 x7 x8 x9 . x6) ⟶ x1 = x3 ⟶ False.
Apply unknownprop_c5c271fc2ac3b14d20f4a11b818283185c3ea9d0e453c95085ee5699f2cf2a6c with
x0,
x1,
λ x4 x5 x6 x7 x8 x9 . x6,
x3 leaving 6 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying unknownprop_9e2647f605c0822439f82a64518aaad84df1ad743ac9deb222cb2ddb0fdd623d.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H7.
Assume H5:
(x0 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ False.
Assume H6:
((λ x4 x5 x6 x7 x8 x9 . x7) = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ (x3 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ False.
Assume H7:
(x0 = λ x4 x5 x6 x7 x8 x9 . x7) ⟶ x1 = x3 ⟶ False.
Apply unknownprop_c5c271fc2ac3b14d20f4a11b818283185c3ea9d0e453c95085ee5699f2cf2a6c with
x0,
x1,
λ x4 x5 x6 x7 x8 x9 . x7,
x3 leaving 6 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying unknownprop_663da7d7e8a8abafb7c1a9461e9654cb1837513857a382d39546c7d9ed1c7389.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H7.
Assume H5:
(x0 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ False.
Assume H6:
((λ x4 x5 x6 x7 x8 x9 . x8) = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ (x3 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ False.
Assume H7:
(x0 = λ x4 x5 x6 x7 x8 x9 . x8) ⟶ x1 = x3 ⟶ False.
Apply unknownprop_c5c271fc2ac3b14d20f4a11b818283185c3ea9d0e453c95085ee5699f2cf2a6c with
x0,
x1,
λ x4 x5 x6 x7 x8 x9 . x8,
x3 leaving 6 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying unknownprop_f25dbc6efc9a35279a230530bfe7a44106f41d1b34b13f2451c96a7a5cd07bae.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H7.
Assume H5:
(x0 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ False.
Assume H6:
((λ x4 x5 x6 x7 x8 x9 . x9) = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ (x3 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ False.
Assume H7:
(x0 = λ x4 x5 x6 x7 x8 x9 . x9) ⟶ x1 = x3 ⟶ False.
Apply unknownprop_205948b2b245cf7ad23e127e884605aea8fc8b571e440a39f68411d75f5d32bf with
x0,
x1,
x3 leaving 5 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying L9.
The subproof is completed by applying H5.
The subproof is completed by applying H7.