Apply unknownprop_cbfb4a8ef037f9166e98e89145be924f54fff8f394689b1e9c22eef2210bedb6 with
u17_to_Church17,
TwoRamseyGraph_3_6_17 leaving 3 subgoals.
The subproof is completed by applying unknownprop_f44342ed74648c23c8734d945bc8b2c1af5a9cb594ef51477e7844cb71f944f8.
The subproof is completed by applying unknownprop_0f7c616bb73771ade29bce8f388fabaa94de35f0c4e10984b06493960171ee05.
Let x0 of type ι be given.
Let x1 of type ι be given.
The subproof is completed by applying H0.