Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ u6.
Let x1 of type ι be given.
Assume H1: x1 ∈ u6.
Let x2 of type ι be given.
Assume H2: x2 ∈ u6.
Let x3 of type ι be given.
Assume H3: x3 ∈ u6.
Assume H4: not (TwoRamseyGraph_4_6_35_a x0 x1 x2 x3).
Assume H5: TwoRamseyGraph_4_6_35_a x2 x3 x0 x1.
Apply H4.
Apply unknownprop_e965020877de1572e3db7225f6e8e02cfdbb951b9add60ee17a78d890a36e854 with x2, x3, x0, x1 leaving 5 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
■