(motive : Int.Linear.Poly → Sort u_1) →
  (x : Int.Linear.Poly) →
    ((v : Int.Linear.Var) → (b : ℤ) → motive (Int.Linear.Poly.add 1 v (Int.Linear.Poly.num b))) →
      ((x : Int.Linear.Poly) → motive x) → motive x