∀ (motive : ℕ → Int.Linear.Poly → Int.Linear.Poly → Int.Linear.Poly → Prop),
  (∀ (p₁ p₂ : Int.Linear.Poly), motive 0 p₁ p₂ (p₁.append p₂)) →
    (∀ (fuel : ℕ) (k₁ k₂ : ℤ),
        motive fuel.succ (Int.Linear.Poly.num k₁) (Int.Linear.Poly.num k₂) (Int.Linear.Poly.num (k₁ + k₂))) →
      (∀ (fuel : ℕ) (k₁ a : ℤ) (x : Int.Linear.Var) (p : Int.Linear.Poly),
          motive fuel (Int.Linear.Poly.num k₁) p (Int.Linear.Poly.combine' fuel (Int.Linear.Poly.num k₁) p) →
            motive fuel.succ (Int.Linear.Poly.num k₁) (Int.Linear.Poly.add a x p)
              (Int.Linear.Poly.add a x (Int.Linear.Poly.combine' fuel (Int.Linear.Poly.num k₁) p))) →
        (∀ (fuel : ℕ) (a : ℤ) (x : Int.Linear.Var) (p : Int.Linear.Poly) (k₂ : ℤ),
            motive fuel p (Int.Linear.Poly.num k₂) (Int.Linear.Poly.combine' fuel p (Int.Linear.Poly.num k₂)) →
              motive fuel.succ (Int.Linear.Poly.add a x p) (Int.Linear.Poly.num k₂)
                (Int.Linear.Poly.add a x (Int.Linear.Poly.combine' fuel p (Int.Linear.Poly.num k₂)))) →
          (∀ (fuel : ℕ) (a₁ : ℤ) (x₁ : Int.Linear.Var) (p₁ : Int.Linear.Poly) (a₂ : ℤ) (x₂ : Int.Linear.Var)
              (p₂ : Int.Linear.Poly),
              Nat.beq x₁ x₂ = true →
                have a := a₁ + a₂;
                (a == 0) = true →
                  motive fuel p₁ p₂ (Int.Linear.Poly.combine' fuel p₁ p₂) →
                    motive fuel.succ (Int.Linear.Poly.add a₁ x₁ p₁) (Int.Linear.Poly.add a₂ x₂ p₂)
                      (Int.Linear.Poly.combine' fuel p₁ p₂)) →
            (∀ (fuel : ℕ) (a₁ : ℤ) (x₁ : Int.Linear.Var) (p₁ : Int.Linear.Poly) (a₂ : ℤ) (x₂ : Int.Linear.Var)
                (p₂ : Int.Linear.Poly),
                Nat.beq x₁ x₂ = true →
                  have a := a₁ + a₂;
                  (a == 0) = false →
                    motive fuel p₁ p₂ (Int.Linear.Poly.combine' fuel p₁ p₂) →
                      motive fuel.succ (Int.Linear.Poly.add a₁ x₁ p₁) (Int.Linear.Poly.add a₂ x₂ p₂)
                        (Int.Linear.Poly.add a x₁ (Int.Linear.Poly.combine' fuel p₁ p₂))) →
              (∀ (fuel : ℕ) (a₁ : ℤ) (x₁ : Int.Linear.Var) (p₁ : Int.Linear.Poly) (a₂ : ℤ) (x₂ : Int.Linear.Var)
                  (p₂ : Int.Linear.Poly),
                  Nat.beq x₁ x₂ = false →
                    Nat.blt x₂ x₁ = true →
                      motive fuel p₁ (Int.Linear.Poly.add a₂ x₂ p₂)
                          (Int.Linear.Poly.combine' fuel p₁ (Int.Linear.Poly.add a₂ x₂ p₂)) →
                        motive fuel.succ (Int.Linear.Poly.add a₁ x₁ p₁) (Int.Linear.Poly.add a₂ x₂ p₂)
                          (Int.Linear.Poly.add a₁ x₁
                            (Int.Linear.Poly.combine' fuel p₁ (Int.Linear.Poly.add a₂ x₂ p₂)))) →
                (∀ (fuel : ℕ) (a₁ : ℤ) (x₁ : Int.Linear.Var) (p₁ : Int.Linear.Poly) (a₂ : ℤ) (x₂ : Int.Linear.Var)
                    (p₂ : Int.Linear.Poly),
                    Nat.beq x₁ x₂ = false →
                      Nat.blt x₂ x₁ = false →
                        motive fuel (Int.Linear.Poly.add a₁ x₁ p₁) p₂
                            (Int.Linear.Poly.combine' fuel (Int.Linear.Poly.add a₁ x₁ p₁) p₂) →
                          motive fuel.succ (Int.Linear.Poly.add a₁ x₁ p₁) (Int.Linear.Poly.add a₂ x₂ p₂)
                            (Int.Linear.Poly.add a₂ x₂
                              (Int.Linear.Poly.combine' fuel (Int.Linear.Poly.add a₁ x₁ p₁) p₂))) →
                  ∀ (fuel : ℕ) (p₁ p₂ : Int.Linear.Poly), motive fuel p₁ p₂ (Int.Linear.Poly.combine' fuel p₁ p₂)