Apply unknownprop_611d05f3c0e0aff033700ccf72b7ceaf4160dd0bd5dde16fbd4a43684d4061b2 with
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.
Let x4 of type ι be given.
Assume H6: x4 ∈ x0.
Let x5 of type ι be given.
Assume H7: x5 ∈ x0.
Assume H8: x1 = x2 ⟶ ∀ x6 : ο . x6.
Assume H9: x1 = x3 ⟶ ∀ x6 : ο . x6.
Assume H10: x1 = x4 ⟶ ∀ x6 : ο . x6.
Assume H11: x1 = x5 ⟶ ∀ x6 : ο . x6.
Assume H12: x2 = x3 ⟶ ∀ x6 : ο . x6.
Assume H13: x2 = x4 ⟶ ∀ x6 : ο . x6.
Assume H14: x2 = x5 ⟶ ∀ x6 : ο . x6.
Assume H15: x3 = x4 ⟶ ∀ x6 : ο . x6.
Assume H16: x3 = x5 ⟶ ∀ x6 : ο . x6.
Assume H17: x4 = x5 ⟶ ∀ x6 : ο . x6.
Apply unknownprop_f13b7928572ea386063941f294a7de5e613d504b56c8df5d720e8c3911580df6 with
x1,
False leaving 2 subgoals.
Apply H0 with
x1.
The subproof is completed by applying H3.
Let x6 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Apply unknownprop_f13b7928572ea386063941f294a7de5e613d504b56c8df5d720e8c3911580df6 with
x2,
False leaving 2 subgoals.
Apply H0 with
x2.
The subproof is completed by applying H4.
Let x7 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Apply unknownprop_f13b7928572ea386063941f294a7de5e613d504b56c8df5d720e8c3911580df6 with
x3,
False leaving 2 subgoals.
Apply H0 with
x3.
The subproof is completed by applying H5.
Let x8 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Apply unknownprop_f13b7928572ea386063941f294a7de5e613d504b56c8df5d720e8c3911580df6 with
x4,
False leaving 2 subgoals.
Apply H0 with
x4.
The subproof is completed by applying H6.
Let x9 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Apply unknownprop_f13b7928572ea386063941f294a7de5e613d504b56c8df5d720e8c3911580df6 with
x5,
False leaving 2 subgoals.
Apply H0 with
x5.
The subproof is completed by applying H7.
Let x10 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Apply unknownprop_354f28a358bf521854ee8b5484a7c25b5b12fa349761b0c407885cb2a055f1f6 with
x9,
x10,
TwoRamseyGraph_3_5_Church13 x9 x10 = λ x11 x12 . x12 leaving 4 subgoals.
The subproof is completed by applying H34.
The subproof is completed by applying H36.
Apply FalseE with
TwoRamseyGraph_3_5_Church13 x9 x10 = λ x11 x12 . x12.
Apply L27.
Let x11 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Let x12 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H60: ....
Apply unknownprop_eaa6acb07f99926ced42ab67baa62f415d6c26fdee92daadab3b8a1c5b203e47 with
x6,
x7,
x8,
x9,
x10 leaving 25 subgoals.
The subproof is completed by applying H28.
The subproof is completed by applying H30.
The subproof is completed by applying H32.
The subproof is completed by applying H34.
The subproof is completed by applying H36.
The subproof is completed by applying L38.
The subproof is completed by applying L39.
The subproof is completed by applying L41.
The subproof is completed by applying L44.
The subproof is completed by applying L40.
The subproof is completed by applying L42.
The subproof is completed by applying L45.
The subproof is completed by applying L43.
The subproof is completed by applying L46.
The subproof is completed by applying L47.
The subproof is completed by applying L48.
The subproof is completed by applying L49.
The subproof is completed by applying L51.
The subproof is completed by applying L54.
The subproof is completed by applying L50.
The subproof is completed by applying L52.
The subproof is completed by applying L55.
The subproof is completed by applying L53.
The subproof is completed by applying L56.
The subproof is completed by applying L57.