Let x0 of type ι be given.
Apply unknownprop_8d334858d1804afd99b1b9082715c7f916daee31e697b66b5c752e0c8756ebae with
x0,
∃ x1 . and (x1 ∈ x0) (x1 ∈ u4) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H6: x1 ∈ x0.
Let x2 of type ι be given.
Assume H7: x2 ∈ x0.
Assume H8: x1 = x2 ⟶ ∀ x3 : ο . x3.
Apply unknownprop_1b81cb9b88d920a0a9ad46bac860e1db1af97240a2a1fd52e148bc0c7ed5adb5 with
u17_to_Church17 x1,
u17_to_Church17 x2,
∃ x3 . and (x3 ∈ x0) (x3 ∈ u4) leaving 11 subgoals.
Apply unknownprop_a1e277f419507eb6211f44d9457aefea2a8b3e26b2ee84f0795856dfe97fcf6e with
x1.
Apply H0 with
x1.
The subproof is completed by applying H6.
Apply unknownprop_a1e277f419507eb6211f44d9457aefea2a8b3e26b2ee84f0795856dfe97fcf6e with
x2.
Apply H0 with
x2.
The subproof is completed by applying H7.
Apply unknownprop_46a7f5ba218e301f19d33cc265134a2df7adfd3de64e750dc665649ee8f6340d with
u17_to_Church17 x1,
λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x16,
TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x16) = λ x3 x4 . x4 leaving 4 subgoals.
The subproof is completed by applying L9.
The subproof is completed by applying unknownprop_d664e656d766635177b954bb19d911f5792a5b476afc9d95f66c535e94450d07.
Apply FalseE with
TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x16) = λ x3 x4 . x4.
Apply H2 with
x1 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply unknownprop_a3161c1a24da07bf7cb898b4bbdd6e6a1dad92a6ebaeb7b53200887c557936fb with
x1,
u13 leaving 3 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying unknownprop_ee249701bfbf4a0ddc5825c1bc6fff36b37e7d1af2b7d307fdfcf229c66eb3d7.
Apply unknownprop_095d0670f988d22364f3d3b9681f2ca00bf954d60116baba131fbf1ee891de57 with
λ x3 x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) x4 = λ x5 x6 . x5.
The subproof is completed by applying H13.
The subproof is completed by applying H13.
Apply unknownprop_46a7f5ba218e301f19d33cc265134a2df7adfd3de64e750dc665649ee8f6340d with
u17_to_Church17 x1,
λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x17,
TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x17) = λ x3 x4 . x4 leaving 4 subgoals.
The subproof is completed by applying L9.
The subproof is completed by applying unknownprop_5749399996f8b07d8783c347f0cf6e04806eba2f6eba6fb3456b8e9db2686cda.
Apply FalseE with
TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x17) = λ x3 x4 . x4.
Apply H3 with
x1 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply unknownprop_a3161c1a24da07bf7cb898b4bbdd6e6a1dad92a6ebaeb7b53200887c557936fb with
x1,
u14 leaving 3 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying unknownprop_19ecd6ac8599e49ad47f95e5b1703b05d2332ac49ec04a48785748b0d8a5094a.
Apply unknownprop_c9b34bc382b6d599e61c555eac34a76c451754eb682c17d99a93f2a1e695d561 with
λ x3 x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) x4 = λ x5 x6 . x5.
The subproof is completed by applying H13.
The subproof is completed by applying H13.
Apply unknownprop_46a7f5ba218e301f19d33cc265134a2df7adfd3de64e750dc665649ee8f6340d with
u17_to_Church17 x1,
λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x18,
TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x18) = λ x3 x4 . x4 leaving 4 subgoals.
The subproof is completed by applying L9.
The subproof is completed by applying unknownprop_9c9197f88eaab6add22634c2b7df334297862a6da7753d0d08affb6802924e7f.
Apply FalseE with
TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x18) = λ x3 x4 . x4.
Apply H4 with
x1 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply unknownprop_a3161c1a24da07bf7cb898b4bbdd6e6a1dad92a6ebaeb7b53200887c557936fb with
x1,
u15 leaving 3 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying unknownprop_35f4d337254964d13bfee3413f1b56f908aee5828cc15d13f416e7a488640c53.
Apply unknownprop_e20cda3fec831e61f9db0bd6bee2791e26067278d174576042c0cb4b3ab479bb with
λ x3 x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) x4 = λ x5 x6 . x5.
The subproof is completed by applying H13.
The subproof is completed by applying H13.
Apply unknownprop_46a7f5ba218e301f19d33cc265134a2df7adfd3de64e750dc665649ee8f6340d with
u17_to_Church17 x2,
λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x16,
TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x16) = λ x3 x4 . x4 leaving 4 subgoals.
The subproof is completed by applying L11.
The subproof is completed by applying unknownprop_d664e656d766635177b954bb19d911f5792a5b476afc9d95f66c535e94450d07.