Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: TwoRamseyGraph_3_6_17 x0 x1.
Assume H1: x1u17.
Assume H2: x0u17.
Apply unknownprop_ee5e0fe730eedc37f764400300b0ed7a640b3bede985cf7ccb67403eb532be1a with u17_to_Church17 x1, u17_to_Church17 x0, λ x2 x3 : ι → ι → ι . x3 = λ x4 x5 . x4 leaving 3 subgoals.
Apply unknownprop_f44342ed74648c23c8734d945bc8b2c1af5a9cb594ef51477e7844cb71f944f8 with x1.
The subproof is completed by applying H1.
Apply unknownprop_f44342ed74648c23c8734d945bc8b2c1af5a9cb594ef51477e7844cb71f944f8 with x0.
The subproof is completed by applying H2.
Apply H0 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.