{α : Type u} →
  {motive : NonUnitalNonAssocCommRing α → Sort u_1} →
    ([toNonUnitalNonAssocRing : NonUnitalNonAssocRing α] →
        (mul_comm : ∀ (a b : α), a * b = b * a) →
          motive { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing, mul_comm := mul_comm }) →
      (t : NonUnitalNonAssocCommRing α) → motive t