Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_14e19ebc7e16f882d3be4482dbe497cecb7597969c9cae0a9f87fe87a0ee217a with
x0,
λ x2 . (TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) (u17_to_Church17 x1) = λ x3 x4 . x3) ⟶ TwoRamseyGraph_3_6_17 x2 x1 leaving 18 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_14e19ebc7e16f882d3be4482dbe497cecb7597969c9cae0a9f87fe87a0ee217a with
x1,
λ x2 . (TwoRamseyGraph_3_6_Church17 (u17_to_Church17 0) (u17_to_Church17 x2) = λ x3 x4 . x3) ⟶ TwoRamseyGraph_3_6_17 0 x2 leaving 18 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H2.
The subproof is completed by applying H2.
Apply unknownprop_84aaefca7211a57d89e0df96a1f742653d3cc05f82d5ab568090ade3cb9ffcfd with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_3_6_Church17 x3 (u17_to_Church17 u3) = λ x4 x5 . x4) ⟶ TwoRamseyGraph_3_6_17 0 u3.
Apply unknownprop_50de3f92839624b98789d3fa24556e40d38a727836b3c2bd366269421355b28d with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_3_6_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x3 = λ x4 x5 . x4) ⟶ TwoRamseyGraph_3_6_17 0 u3.
Assume H2:
TwoRamseyGraph_3_6_Church17 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x5) = λ x2 x3 . x2.
Apply FalseE with
TwoRamseyGraph_3_6_17 0 u3.
Apply unknownprop_1019f796b5519c5beeeef55b1daae2de48848a97e75d217687db0a2449fd5208.
The subproof is completed by applying H2.
Apply unknownprop_84aaefca7211a57d89e0df96a1f742653d3cc05f82d5ab568090ade3cb9ffcfd with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_3_6_Church17 x3 (u17_to_Church17 u4) = λ x4 x5 . x4) ⟶ TwoRamseyGraph_3_6_17 0 u4.
Apply unknownprop_f6f6b2d4f503fb9b975e320862d0437f04a94f96cc19149de839c0a7d55394f3 with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_3_6_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x3 = λ x4 x5 . x4) ⟶ TwoRamseyGraph_3_6_17 0 u4.
Assume H2:
TwoRamseyGraph_3_6_Church17 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x6) = λ x2 x3 . x2.
Apply FalseE with
TwoRamseyGraph_3_6_17 0 u4.
Apply unknownprop_1019f796b5519c5beeeef55b1daae2de48848a97e75d217687db0a2449fd5208.
The subproof is completed by applying H2.
Apply unknownprop_84aaefca7211a57d89e0df96a1f742653d3cc05f82d5ab568090ade3cb9ffcfd with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_3_6_Church17 x3 (u17_to_Church17 u5) = λ x4 x5 . x4) ⟶ TwoRamseyGraph_3_6_17 0 u5.
Apply unknownprop_ccd09fc33db26fba17a1e8f5fd52159b676a35cf5706e2e445b9db64b4fc35c5 with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_3_6_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x3 = λ x4 x5 . x4) ⟶ TwoRamseyGraph_3_6_17 0 u5.
Assume H2:
TwoRamseyGraph_3_6_Church17 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x7) = λ x2 x3 . x2.
Apply FalseE with
TwoRamseyGraph_3_6_17 0 u5.
Apply unknownprop_1019f796b5519c5beeeef55b1daae2de48848a97e75d217687db0a2449fd5208.
The subproof is completed by applying H2.
Apply unknownprop_84aaefca7211a57d89e0df96a1f742653d3cc05f82d5ab568090ade3cb9ffcfd with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_3_6_Church17 x3 (u17_to_Church17 u6) = λ x4 x5 . x4) ⟶ TwoRamseyGraph_3_6_17 0 u6.
Apply unknownprop_b2c765c786aca76bfef751038ffbb16620c4c7136061de036517f3c71ce2abfd with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_3_6_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x3 = λ x4 x5 . x4) ⟶ TwoRamseyGraph_3_6_17 0 u6.
Assume H2:
TwoRamseyGraph_3_6_Church17 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x8) = λ x2 x3 . x2.
Apply FalseE with
TwoRamseyGraph_3_6_17 0 u6.
Apply unknownprop_1019f796b5519c5beeeef55b1daae2de48848a97e75d217687db0a2449fd5208.
The subproof is completed by applying H2.
The subproof is completed by applying H2.
Apply unknownprop_84aaefca7211a57d89e0df96a1f742653d3cc05f82d5ab568090ade3cb9ffcfd with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_3_6_Church17 x3 (u17_to_Church17 u8) = λ x4 x5 . x4) ⟶ TwoRamseyGraph_3_6_17 0 u8.
Apply unknownprop_8f7d877f09ad2d2b6bd165b15d072d92366514d5c83c4caef2b25c48dd454e7b with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_3_6_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x3 = λ x4 x5 . x4) ⟶ TwoRamseyGraph_3_6_17 0 u8.