{α : Type u_5} →
  {motive : SeminormedCommRing α → Sort u} →
    (t : SeminormedCommRing α) →
      ([toSeminormedRing : SeminormedRing α] →
          (mul_comm : ∀ (a b : α), a * b = b * a) →
            motive { toSeminormedRing := toSeminormedRing, mul_comm := mul_comm }) →
        motive t