Let x0 of type ι be given.
Apply unknownprop_95c6cbd2308b27a7edcd2a1d9389b377988e902d740d05dc7c88e6b8da945ab9 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 H3: x1 ∈ x0.
Let x2 of type ι be given.
Assume H4: x2 ∈ x0.
Let x3 of type ι be given.
Assume H5: x3 ∈ x0.
Assume H6: x1 = x2 ⟶ ∀ x4 : ο . x4.
Assume H7: x1 = x3 ⟶ ∀ x4 : ο . x4.
Assume H8: x2 = x3 ⟶ ∀ x4 : ο . x4.
Apply unknownprop_61ddddc19337f8e85511960b4f5775d8168a24f8064036ba92bb977d6d36d871 with
u17_to_Church17 x1,
u17_to_Church17 x2,
u17_to_Church17 x3,
∃ x4 . and (x4 ∈ x0) (x4 ∈ u4) leaving 9 subgoals.
The subproof is completed by applying L9.
The subproof is completed by applying L11.
Apply unknownprop_a1e277f419507eb6211f44d9457aefea2a8b3e26b2ee84f0795856dfe97fcf6e with
x3.
Apply H0 with
x3.
The subproof is completed by applying H5.
Apply unknownprop_46a7f5ba218e301f19d33cc265134a2df7adfd3de64e750dc665649ee8f6340d with
u17_to_Church17 x1,
u17_to_Church17 x2,
TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (u17_to_Church17 x2) = λ x4 x5 . x5 leaving 4 subgoals.
Apply unknownprop_2fa525e41523fb22ae024d24b945825c4a3fbfd79f9bf422589dd3f334717095 with
u17_to_Church17 x1.
The subproof is completed by applying L9.
Apply unknownprop_2fa525e41523fb22ae024d24b945825c4a3fbfd79f9bf422589dd3f334717095 with
u17_to_Church17 x2.
The subproof is completed by applying L11.
Apply FalseE with
TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (u17_to_Church17 x2) = λ x4 x5 . x5.
Apply H2 with
x1,
x2 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
Apply unknownprop_a3161c1a24da07bf7cb898b4bbdd6e6a1dad92a6ebaeb7b53200887c557936fb with
x1,
x2 leaving 3 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying L12.
The subproof is completed by applying H14.
The subproof is completed by applying H14.
Apply unknownprop_46a7f5ba218e301f19d33cc265134a2df7adfd3de64e750dc665649ee8f6340d with
u17_to_Church17 x1,
u17_to_Church17 x3,
TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (u17_to_Church17 x3) = λ x4 x5 . x5 leaving 4 subgoals.
Apply unknownprop_2fa525e41523fb22ae024d24b945825c4a3fbfd79f9bf422589dd3f334717095 with
u17_to_Church17 x1.
The subproof is completed by applying L9.
Apply unknownprop_2fa525e41523fb22ae024d24b945825c4a3fbfd79f9bf422589dd3f334717095 with
u17_to_Church17 x3.
Apply unknownprop_a1e277f419507eb6211f44d9457aefea2a8b3e26b2ee84f0795856dfe97fcf6e with
x3.
Apply H0 with
x3.
The subproof is completed by applying H5.
Apply FalseE with
TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (u17_to_Church17 x3) = λ x4 x5 . x5.
Apply H2 with
x1,
x3 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying H7.
Apply unknownprop_a3161c1a24da07bf7cb898b4bbdd6e6a1dad92a6ebaeb7b53200887c557936fb with
x1,
x3 leaving 3 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying L13.
The subproof is completed by applying H14.
The subproof is completed by applying H14.
Apply unknownprop_46a7f5ba218e301f19d33cc265134a2df7adfd3de64e750dc665649ee8f6340d with
u17_to_Church17 x2,
u17_to_Church17 x3,
TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) (u17_to_Church17 x3) = λ x4 x5 . x5 leaving 4 subgoals.
Apply unknownprop_2fa525e41523fb22ae024d24b945825c4a3fbfd79f9bf422589dd3f334717095 with
u17_to_Church17 x2.
The subproof is completed by applying L11.
Apply unknownprop_2fa525e41523fb22ae024d24b945825c4a3fbfd79f9bf422589dd3f334717095 with
u17_to_Church17 x3.
Apply unknownprop_a1e277f419507eb6211f44d9457aefea2a8b3e26b2ee84f0795856dfe97fcf6e with
x3.
Apply H0 with
x3.
The subproof is completed by applying H5.
Apply FalseE with
TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) (u17_to_Church17 x3) = λ x4 x5 . x5.
Apply H2 with
x2,
x3 leaving 4 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H8.
Apply unknownprop_a3161c1a24da07bf7cb898b4bbdd6e6a1dad92a6ebaeb7b53200887c557936fb with
x2,
x3 leaving 3 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying L13.
The subproof is completed by applying H14.
The subproof is completed by applying H14.
Let x4 of type ο be given.
Assume H15:
∀ x5 . and (x5 ∈ x0) (x5 ∈ u4) ⟶ x4.
Apply H15 with
x1.
Apply andI with
x1 ∈ x0,
x1 ∈ u4 leaving 2 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_35525b8462c5f0502572f7a7d201d6eac29160ec2643e45e6a1e8008a8129eba with
x1 leaving 2 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying H14.
Let x4 of type ο be given.
Assume H15:
∀ x5 . and (x5 ∈ x0) (x5 ∈ u4) ⟶ x4.