Apply unknownprop_5b7536e138ce2802b7ff71fe1112d72a83e0e7fe4b94027c8a3d1f1cacfae786 with
5,
5,
prim4 7,
prim4 8 leaving 2 subgoals.
The subproof is completed by applying unknownprop_ed9ae380d91bb4eef6a9133f8865237c6a1236bcf056f5e6c2e3787bb8a1ba4a with 7.
The subproof is completed by applying TwoRamseyProp_5_5_Power_7.