∀ {v : Lean.Level} {M : Q(Type v)} (motive : Mathlib.Tactic.FieldSimp.qNF M → Mathlib.Tactic.FieldSimp.qNF M → Sort u_1)
  (a₁ : ℤ) (x₁ : Q(«$M»)) (k₁ : ℕ) (t₁ : List ((ℤ × Q(«$M»)) × ℕ)) (a₂ : ℤ) (x₂ : Q(«$M»)) (k₂ : ℕ)
  (t₂ : List ((ℤ × Q(«$M»)) × ℕ)) (h_1 : (l : Mathlib.Tactic.FieldSimp.qNF M) → motive [] l)
  (h_2 : (l : Mathlib.Tactic.FieldSimp.qNF M) → motive l [])
  (h_3 :
    (a₁ : ℤ) →
      (x₁ : Q(«$M»)) →
        (k₁ : ℕ) →
          (t₁ : List ((ℤ × Q(«$M»)) × ℕ)) →
            (a₂ : ℤ) →
              (x₂ : Q(«$M»)) →
                (k₂ : ℕ) → (t₂ : List ((ℤ × Q(«$M»)) × ℕ)) → motive (((a₁, x₁), k₁) :: t₁) (((a₂, x₂), k₂) :: t₂)),
  (match ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ with
    | [], l => h_1 l
    | l, [] => h_2 l
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ => h_3 a₁ x₁ k₁ t₁ a₂ x₂ k₂ t₂) =
    h_3 a₁ x₁ k₁ t₁ a₂ x₂ k₂ t₂