{G : Type u} →
  {P : Sort u_1} →
    {toGroup : Group G} →
      {mul_comm : ∀ (a b : G), a * b = b * a} →
        {toGroup' : Group G} →
          {mul_comm' : ∀ (a b : G), a * b = b * a} →
            { toGroup := toGroup, mul_comm := mul_comm } = { toGroup := toGroup', mul_comm := mul_comm' } →
              (toGroup ≍ toGroup' → P) → P