Apply unknownprop_5b7536e138ce2802b7ff71fe1112d72a83e0e7fe4b94027c8a3d1f1cacfae786 with
3,
6,
prim4 6,
prim4 7 leaving 2 subgoals.
The subproof is completed by applying unknownprop_ed9ae380d91bb4eef6a9133f8865237c6a1236bcf056f5e6c2e3787bb8a1ba4a with 6.
The subproof is completed by applying TwoRamseyProp_3_6_Power_6.