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 H5: x1 ∈ x0.
Let x2 of type ι be given.
Assume H6: x2 ∈ x0.
Assume H7: x1 = x2 ⟶ ∀ x3 : ο . x3.
Apply unknownprop_9c873b1bebbbdb754d62c8f5390d28f666ffc7ed328c5c9f91dcd453febe0e1f with
u17_to_Church17 x1,
u17_to_Church17 x2,
∃ x3 . and (x3 ∈ x0) (x3 ∈ u4) leaving 9 subgoals.
Apply unknownprop_a1e277f419507eb6211f44d9457aefea2a8b3e26b2ee84f0795856dfe97fcf6e with
x1.
Apply H0 with
x1.
The subproof is completed by applying H5.
Apply unknownprop_a1e277f419507eb6211f44d9457aefea2a8b3e26b2ee84f0795856dfe97fcf6e with
x2.
Apply H0 with
x2.
The subproof is completed by applying H6.
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 . x11,
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 . x11) = λ x3 x4 . x4 leaving 4 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying unknownprop_c37600b80efb18922b2424c0ae3622d88c262b6e7e6fb3aa0f6bc2b0ba9f1be7.
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 . x11) = λ x3 x4 . x4.
Apply H2 with
x1 leaving 2 subgoals.
The subproof is completed by applying H5.
Apply unknownprop_a3161c1a24da07bf7cb898b4bbdd6e6a1dad92a6ebaeb7b53200887c557936fb with
x1,
u8 leaving 3 subgoals.
The subproof is completed by applying L9.
The subproof is completed by applying unknownprop_6e6799a9f21ccdffe58af218db8306610bd1441f3fa0fcc3f6eaa957ce165f57.
Apply unknownprop_8f7d877f09ad2d2b6bd165b15d072d92366514d5c83c4caef2b25c48dd454e7b with
λ x3 x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) x4 = λ x5 x6 . x5.
The subproof is completed by applying H12.
The subproof is completed by applying H12.
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 . x12,
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 . x12) = λ x3 x4 . x4 leaving 4 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying unknownprop_7fcbe5b61ad12e38a6853aaa6fe3dd0299d75fe061e77a480a4e344498540b83.
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 . x12) = λ x3 x4 . x4.
Apply H3 with
x1 leaving 2 subgoals.
The subproof is completed by applying H5.
Apply unknownprop_a3161c1a24da07bf7cb898b4bbdd6e6a1dad92a6ebaeb7b53200887c557936fb with
x1,
u9 leaving 3 subgoals.
The subproof is completed by applying L9.
The subproof is completed by applying unknownprop_abbef1301044c000653f42960a8047881f2ef656bd9cecef0ae9b764b6c0784f.
Apply unknownprop_08c2582e457fa5da2b4ee2676b94e0e9b149b350b636df86eee53e8e8dded2c1 with
λ x3 x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) x4 = λ x5 x6 . x5.
The subproof is completed by applying H12.
The subproof is completed by applying H12.
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 . x11,
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 . x11) = λ x3 x4 . x4 leaving 4 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying unknownprop_c37600b80efb18922b2424c0ae3622d88c262b6e7e6fb3aa0f6bc2b0ba9f1be7.
Apply FalseE with
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 . x11) = λ x3 x4 . x4.
Apply H2 with
x2 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply unknownprop_a3161c1a24da07bf7cb898b4bbdd6e6a1dad92a6ebaeb7b53200887c557936fb with
x2,
u8 leaving 3 subgoals.
The subproof is completed by applying L11.
The subproof is completed by applying unknownprop_6e6799a9f21ccdffe58af218db8306610bd1441f3fa0fcc3f6eaa957ce165f57.
Apply unknownprop_8f7d877f09ad2d2b6bd165b15d072d92366514d5c83c4caef2b25c48dd454e7b with
λ x3 x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) x4 = λ x5 x6 . x5.
The subproof is completed by applying H12.
The subproof is completed by applying H12.
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 . x12,
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 . x12) = λ x3 x4 . x4 leaving 4 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying unknownprop_7fcbe5b61ad12e38a6853aaa6fe3dd0299d75fe061e77a480a4e344498540b83.
Apply FalseE with
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 . x12) = λ x3 x4 . x4.
Apply H3 with
x2 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply unknownprop_a3161c1a24da07bf7cb898b4bbdd6e6a1dad92a6ebaeb7b53200887c557936fb with
x2,
u9 leaving 3 subgoals.
The subproof is completed by applying L11.