{α : Type u_5} →
  {motive : NonUnitalSeminormedCommRing α → Sort u} →
    (t : NonUnitalSeminormedCommRing α) →
      ([toNonUnitalSeminormedRing : NonUnitalSeminormedRing α] →
          (mul_comm : ∀ (a b : α), a * b = b * a) →
            motive { toNonUnitalSeminormedRing := toNonUnitalSeminormedRing, mul_comm := mul_comm }) →
        motive t