{m : Type → Type} →
  {motive : Lean.Meta.Grind.Arith.CommRing.MonadCommRing m → Sort u} →
    (t : Lean.Meta.Grind.Arith.CommRing.MonadCommRing m) →
      ((getCommRing : m Lean.Meta.Grind.Arith.CommRing.CommRing) →
          (modifyCommRing :
              (Lean.Meta.Grind.Arith.CommRing.CommRing → Lean.Meta.Grind.Arith.CommRing.CommRing) → m Unit) →
            motive { getCommRing := getCommRing, modifyCommRing := modifyCommRing }) →
        motive t