Apply unknownprop_3a70dad70ca002c7b398c98a1388fa0229d3bf05a40f90c8db063d0ec2c78284.
Apply TwoRamseyProp_atleastp_atleastp with
u3,
u3,
u7,
u7,
u22 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying atleastp_ref with
u3.
The subproof is completed by applying atleastp_ref with
u7.