∀ (motive : (_ : Lean.Grind.Linarith.Poly) ×' Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Prop),
  (∀ (p₂ : Lean.Grind.Linarith.Poly), motive ⟨Lean.Grind.Linarith.Poly.nil, p₂⟩ p₂) →
    (∀ (p₁ : Lean.Grind.Linarith.Poly),
        (p₁ = Lean.Grind.Linarith.Poly.nil → False) → motive ⟨p₁, Lean.Grind.Linarith.Poly.nil⟩ p₁) →
      (∀ (a₁ : ℤ) (x₁ : Lean.Grind.Linarith.Var) (p₁ : Lean.Grind.Linarith.Poly) (a₂ : ℤ) (x₂ : Lean.Grind.Linarith.Var)
          (p₂ : Lean.Grind.Linarith.Poly),
          Nat.beq x₁ x₂ = true →
            have a := a₁ + a₂;
            (a == 0) = true →
              motive ⟨p₁, p₂⟩ (Lean.Grind.Linarith.Poly.combine._unary ⟨p₁, p₂⟩) →
                motive ⟨Lean.Grind.Linarith.Poly.add a₁ x₁ p₁, Lean.Grind.Linarith.Poly.add a₂ x₂ p₂⟩
                  (Lean.Grind.Linarith.Poly.combine._unary ⟨p₁, p₂⟩)) →
        (∀ (a₁ : ℤ) (x₁ : Lean.Grind.Linarith.Var) (p₁ : Lean.Grind.Linarith.Poly) (a₂ : ℤ)
            (x₂ : Lean.Grind.Linarith.Var) (p₂ : Lean.Grind.Linarith.Poly),
            Nat.beq x₁ x₂ = true →
              have a := a₁ + a₂;
              (a == 0) = false →
                motive ⟨p₁, p₂⟩ (Lean.Grind.Linarith.Poly.combine._unary ⟨p₁, p₂⟩) →
                  motive ⟨Lean.Grind.Linarith.Poly.add a₁ x₁ p₁, Lean.Grind.Linarith.Poly.add a₂ x₂ p₂⟩
                    (Lean.Grind.Linarith.Poly.add a x₁ (Lean.Grind.Linarith.Poly.combine._unary ⟨p₁, p₂⟩))) →
          (∀ (a₁ : ℤ) (x₁ : Lean.Grind.Linarith.Var) (p₁ : Lean.Grind.Linarith.Poly) (a₂ : ℤ)
              (x₂ : Lean.Grind.Linarith.Var) (p₂ : Lean.Grind.Linarith.Poly),
              Nat.beq x₁ x₂ = false →
                Nat.blt x₂ x₁ = true →
                  motive ⟨p₁, Lean.Grind.Linarith.Poly.add a₂ x₂ p₂⟩
                      (Lean.Grind.Linarith.Poly.combine._unary ⟨p₁, Lean.Grind.Linarith.Poly.add a₂ x₂ p₂⟩) →
                    motive ⟨Lean.Grind.Linarith.Poly.add a₁ x₁ p₁, Lean.Grind.Linarith.Poly.add a₂ x₂ p₂⟩
                      (Lean.Grind.Linarith.Poly.add a₁ x₁
                        (Lean.Grind.Linarith.Poly.combine._unary ⟨p₁, Lean.Grind.Linarith.Poly.add a₂ x₂ p₂⟩))) →
            (∀ (a₁ : ℤ) (x₁ : Lean.Grind.Linarith.Var) (p₁ : Lean.Grind.Linarith.Poly) (a₂ : ℤ)
                (x₂ : Lean.Grind.Linarith.Var) (p₂ : Lean.Grind.Linarith.Poly),
                Nat.beq x₁ x₂ = false →
                  Nat.blt x₂ x₁ = false →
                    motive ⟨Lean.Grind.Linarith.Poly.add a₁ x₁ p₁, p₂⟩
                        (Lean.Grind.Linarith.Poly.combine._unary ⟨Lean.Grind.Linarith.Poly.add a₁ x₁ p₁, p₂⟩) →
                      motive ⟨Lean.Grind.Linarith.Poly.add a₁ x₁ p₁, Lean.Grind.Linarith.Poly.add a₂ x₂ p₂⟩
                        (Lean.Grind.Linarith.Poly.add a₂ x₂
                          (Lean.Grind.Linarith.Poly.combine._unary ⟨Lean.Grind.Linarith.Poly.add a₁ x₁ p₁, p₂⟩))) →
              ∀ (_x : (_ : Lean.Grind.Linarith.Poly) ×' Lean.Grind.Linarith.Poly),
                motive _x (Lean.Grind.Linarith.Poly.combine._unary _x)