(motive :
    Mathlib.Tactic.Linarith.ExprMap →
      List Lean.Expr → Mathlib.Tactic.Linarith.Map Mathlib.Tactic.Linarith.Monom ℕ → Sort u_1) →
  (x : Mathlib.Tactic.Linarith.ExprMap) →
    (x_1 : List Lean.Expr) →
      (x_2 : Mathlib.Tactic.Linarith.Map Mathlib.Tactic.Linarith.Monom ℕ) →
        ((m : Mathlib.Tactic.Linarith.ExprMap) →
            (mm : Mathlib.Tactic.Linarith.Map Mathlib.Tactic.Linarith.Monom ℕ) → motive m [] mm) →
          ((m : Mathlib.Tactic.Linarith.ExprMap) →
              (h : Lean.Expr) →
                (t : List Lean.Expr) →
                  (mm : Mathlib.Tactic.Linarith.Map Mathlib.Tactic.Linarith.Monom ℕ) → motive m (h :: t) mm) →
            motive x x_1 x_2