{P : Sort u} →
  {k : ℤ} →
    {v : Lean.Grind.Linarith.Var} →
      {p : Lean.Grind.Linarith.Poly} →
        {k' : ℤ} →
          {v' : Lean.Grind.Linarith.Var} →
            {p' : Lean.Grind.Linarith.Poly} →
              Lean.Grind.Linarith.Poly.add k v p = Lean.Grind.Linarith.Poly.add k' v' p' →
                (k = k' → v = v' → p = p' → P) → P