{u v : Lean.Level} →
  {M : Q(Type v)} →
    {R : Q(Type u)} →
      (motive : Mathlib.Tactic.Module.qNF R M → Mathlib.Tactic.Module.qNF R M → Sort u_1) →
        (x x_1 : Mathlib.Tactic.Module.qNF R M) →
          ((l : Mathlib.Tactic.Module.qNF R M) → motive [] l) →
            ((l : Mathlib.Tactic.Module.qNF R M) → motive l []) →
              ((a₁ : Q(«$R»)) →
                  (x₁ : Q(«$M»)) →
                    (k₁ : ℕ) →
                      (t₁ : Mathlib.Tactic.Module.NF (Q(«$R») × Q(«$M»)) ℕ) →
                        (a₂ : Q(«$R»)) →
                          (x₂ : Q(«$M»)) →
                            (k₂ : ℕ) →
                              (t₂ : Mathlib.Tactic.Module.NF (Q(«$R») × Q(«$M»)) ℕ) →
                                motive (((a₁, x₁), k₁) :: t₁) (((a₂, x₂), k₂) :: t₂)) →
                motive x x_1