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