Claim L0: ((λ x0 x1 . x1) = λ x0 x1 . x0) ⟶ ∀ x0 : ο . x0
The subproof is completed by applying unknownprop_1019f796b5519c5beeeef55b1daae2de48848a97e75d217687db0a2449fd5208.
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) ⟶ (x4 = x2 ⟶ x1 = x3 ⟶ False) ⟶ (TwoRamseyGraph_4_6_Church6_squared_a x4 x1 x2 x3 = λ x5 x6 . x5) ⟶ TwoRamseyGraph_4_6_Church6_squared_b 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_e3faf03657b0d29214ed21048f018ef11905efd48e576ac36e5667597507679e 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_e3faf03657b0d29214ed21048f018ef11905efd48e576ac36e5667597507679e 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_e3faf03657b0d29214ed21048f018ef11905efd48e576ac36e5667597507679e 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_e3faf03657b0d29214ed21048f018ef11905efd48e576ac36e5667597507679e 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_e3faf03657b0d29214ed21048f018ef11905efd48e576ac36e5667597507679e 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.
Assume H5:
((λ x4 x5 x6 x7 x8 x9 . x9) = λ 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) = x2 ⟶ x1 = x3 ⟶ False.
Apply unknownprop_fc3a257d01c5d8b689222fd0e81170fd80e24606b911d53b0c7e9cb42af45680 with
x1,
x2,
x3 leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Assume H7: x1 = λ x4 x5 x6 x7 x8 x9 . x9.
Apply H5 leaving 2 subgoals.
Let x4 of type (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο be given.
Assume H8: x4 (λ x5 x6 x7 x8 x9 x10 . x10) (λ x5 x6 x7 x8 x9 x10 . x10).
The subproof is completed by applying H8.
The subproof is completed by applying H7.