(motive : Option Int.Linear.Expr → Int.Linear.Poly → Sort u_1) →
  (x : Option Int.Linear.Expr) →
    (x_1 : Int.Linear.Poly) →
      ((k : ℤ) → motive none (Int.Linear.Poly.num k)) →
        ((e : Int.Linear.Expr) → motive (some e) (Int.Linear.Poly.num 0)) →
          ((e : Int.Linear.Expr) → (k : ℤ) → motive (some e) (Int.Linear.Poly.num k)) →
            ((x : Int.Linear.Var) → (p : Int.Linear.Poly) → motive none (Int.Linear.Poly.add 1 x p)) →
              ((k : ℤ) → (x : Int.Linear.Var) → (p : Int.Linear.Poly) → motive none (Int.Linear.Poly.add k x p)) →
                ((e : Int.Linear.Expr) →
                    (x : Int.Linear.Var) → (p : Int.Linear.Poly) → motive (some e) (Int.Linear.Poly.add 1 x p)) →
                  ((e : Int.Linear.Expr) →
                      (k : ℤ) →
                        (x : Int.Linear.Var) → (p : Int.Linear.Poly) → motive (some e) (Int.Linear.Poly.add k x p)) →
                    motive x x_1