{α : Type u} →
  {motive : NonAssocCommSemiring α → Sort u_1} →
    (t : NonAssocCommSemiring α) →
      ([toNonAssocSemiring : NonAssocSemiring α] →
          (mul_comm : ∀ (a b : α), a * b = b * a) →
            motive { toNonAssocSemiring := toNonAssocSemiring, mul_comm := mul_comm }) →
        motive t