Apply unknownprop_5b7536e138ce2802b7ff71fe1112d72a83e0e7fe4b94027c8a3d1f1cacfae786 with
4,
4,
prim4 5,
prim4 6 leaving 2 subgoals.
The subproof is completed by applying unknownprop_ed9ae380d91bb4eef6a9133f8865237c6a1236bcf056f5e6c2e3787bb8a1ba4a with 5.
The subproof is completed by applying TwoRamseyProp_4_4_Power_5.