∀ (m : Lean.Grind.CommRing.Mon) (x : Lean.Grind.CommRing.Var),
  m.cancelVar x =
    match m with
    | Lean.Grind.CommRing.Mon.unit => Lean.Grind.CommRing.Mon.unit
    | Lean.Grind.CommRing.Mon.mult pw m => bif pw.x == x then m else Lean.Grind.CommRing.Mon.mult pw (m.cancelVar x)