{G : Type u} →
  {P : Sort u_1} →
    {toSemigroup : Semigroup G} →
      {toIsRightCancelMul : IsRightCancelMul G} →
        {toSemigroup' : Semigroup G} →
          {toIsRightCancelMul' : IsRightCancelMul G} →
            { toSemigroup := toSemigroup, toIsRightCancelMul := toIsRightCancelMul } =
                { toSemigroup := toSemigroup', toIsRightCancelMul := toIsRightCancelMul' } →
              (toSemigroup ≍ toSemigroup' → P) → P