Let x0 of type ι be given.
Assume H0: x0 ∈ 17.
Let x1 of type ι be given.
Assume H1: x1 ∈ 17.
Assume H2: x0 = x1 ⟶ ∀ x2 : ο . x2.
The subproof is completed by applying H3.
Apply unknownprop_1834b85271c8875943c2ffcc84c12f5fbb059bb64cc7b431c141c0353370cd27 with
u17_to_Church17,
TwoRamseyGraph_3_6_17 leaving 8 subgoals.
The subproof is completed by applying unknownprop_d33ea914c01284b1fc49147f7bcc51527f787dcf89c80cfdad2e5f419cbe1dbb.
The subproof is completed by applying unknownprop_095d0670f988d22364f3d3b9681f2ca00bf954d60116baba131fbf1ee891de57.
The subproof is completed by applying unknownprop_c9b34bc382b6d599e61c555eac34a76c451754eb682c17d99a93f2a1e695d561.
The subproof is completed by applying unknownprop_e20cda3fec831e61f9db0bd6bee2791e26067278d174576042c0cb4b3ab479bb.
The subproof is completed by applying unknownprop_2491d2eab9fb9ff25fa0ab1839a83bd77980933cdf40d8cdd9120c539e464911.
The subproof is completed by applying L0.
The subproof is completed by applying unknownprop_82a4043338dce48d58934c215ccdbe85be545db6869ac125d5e92b153cac28bb.
The subproof is completed by applying unknownprop_dd20968590d1b4c22778c64bd2299c3d4b76c5d3d25dcc77c8be400e32088802.