(motive : Int.Linear.Poly → Sort u_1) →
  (p : Int.Linear.Poly) →
    ((a : ℤ) → (y : Int.Linear.Var) → (p : Int.Linear.Poly) → motive (Int.Linear.Poly.add a y p)) →
      ((k : ℤ) → motive (Int.Linear.Poly.num k)) → motive p