∀ (motive : ℤ → Int.Linear.Expr → Prop),
  (∀ (coeff k : ℤ), (k == 0) = true → motive coeff (Int.Linear.Expr.num k)) →
    (∀ (coeff k : ℤ), (k == 0) = false → motive coeff (Int.Linear.Expr.num k)) →
      (∀ (coeff : ℤ) (v : Int.Linear.Var), motive coeff (Int.Linear.Expr.var v)) →
        (∀ (coeff : ℤ) (a b : Int.Linear.Expr), motive coeff a → motive coeff b → motive coeff (a.add b)) →
          (∀ (coeff : ℤ) (a b : Int.Linear.Expr), motive coeff a → motive (-coeff) b → motive coeff (a.sub b)) →
            (∀ (coeff k : ℤ) (a : Int.Linear.Expr), (k == 0) = true → motive coeff (Int.Linear.Expr.mulL k a)) →
              (∀ (coeff k : ℤ) (a : Int.Linear.Expr),
                  (k == 0) = false → motive (coeff.mul k) a → motive coeff (Int.Linear.Expr.mulL k a)) →
                (∀ (coeff : ℤ) (a : Int.Linear.Expr) (k : ℤ), (k == 0) = true → motive coeff (a.mulR k)) →
                  (∀ (coeff : ℤ) (a : Int.Linear.Expr) (k : ℤ),
                      (k == 0) = false → motive (coeff.mul k) a → motive coeff (a.mulR k)) →
                    (∀ (coeff : ℤ) (a : Int.Linear.Expr), motive (-coeff) a → motive coeff a.neg) →
                      ∀ (coeff : ℤ) (a : Int.Linear.Expr), motive coeff a