(motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) →
  (x x_1 : Lean.Grind.CommRing.Mon) →
    ((m₁ : Lean.Grind.CommRing.Mon) → motive m₁ Lean.Grind.CommRing.Mon.unit) →
      ((x : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit x) →
        ((pw₁ : Lean.Grind.CommRing.Power) →
            (m₁ : Lean.Grind.CommRing.Mon) →
              (pw₂ : Lean.Grind.CommRing.Power) →
                (m₂ : Lean.Grind.CommRing.Mon) →
                  motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)) →
          motive x x_1