∀ (motive : Int.Linear.Poly → Int.Linear.Poly → Sort u_1) (p₁ p₂ : Int.Linear.Poly)
  (h_1 : (k₁ k₂ : ℤ) → motive (Int.Linear.Poly.num k₁) (Int.Linear.Poly.num k₂))
  (h_2 :
    (k₁ a : ℤ) →
      (x : Int.Linear.Var) → (p : Int.Linear.Poly) → motive (Int.Linear.Poly.num k₁) (Int.Linear.Poly.add a x p))
  (h_3 :
    (a : ℤ) →
      (x : Int.Linear.Var) →
        (p : Int.Linear.Poly) → (k₂ : ℤ) → motive (Int.Linear.Poly.add a x p) (Int.Linear.Poly.num k₂))
  (h_4 :
    (a₁ : ℤ) →
      (x₁ : Int.Linear.Var) →
        (p₁ : Int.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Linear.Var) →
              (p₂ : Int.Linear.Poly) → motive (Int.Linear.Poly.add a₁ x₁ p₁) (Int.Linear.Poly.add a₂ x₂ p₂))
  (a : ℤ) (x : Int.Linear.Var) (p : Int.Linear.Poly) (k₂ : ℤ),
  p₁ = Int.Linear.Poly.add a x p →
    p₂ = Int.Linear.Poly.num k₂ →
      (match p₁, p₂ with
        | Int.Linear.Poly.num k₁, Int.Linear.Poly.num k₂ => h_1 k₁ k₂
        | Int.Linear.Poly.num k₁, Int.Linear.Poly.add a x p => h_2 k₁ a x p
        | Int.Linear.Poly.add a x p, Int.Linear.Poly.num k₂ => h_3 a x p k₂
        | Int.Linear.Poly.add a₁ x₁ p₁, Int.Linear.Poly.add a₂ x₂ p₂ => h_4 a₁ x₁ p₁ a₂ x₂ p₂) ≍
        h_3 a x p k₂