∀ {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} (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»)) ℕ),
  (invImage (fun x => PSigma.casesOn x fun a a_1 => (a, a_1)) Prod.instWellFoundedRelation).1
    ⟨t₁, ((a₂, x₂), k₂) ::ᵣ t₂⟩ ⟨((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂⟩