∀ {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} (iR : Q(Ring «$R»)) (iM : Q(AddCommGroup «$M»))
  (iRM : Q(Module «$R» «$M»)) (l₁ l₂ : Mathlib.Tactic.Module.qNF R M),
  Mathlib.Tactic.Module.qNF.mkSubProof iR iM iRM l₁ l₂ =
    match l₁, l₂ with
    | [], l =>
      have a := l.toNF;
      q(⋯)
    | l, [] =>
      have a := l.toNF;
      q(⋯)
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ =>
      if k₁ < k₂ then
        have pf := Mathlib.Tactic.Module.qNF.mkSubProof iR iM iRM t₁ (((a₂, x₂), k₂) ::ᵣ t₂);
        q(⋯)
      else
        if k₁ = k₂ then
          have pf := Mathlib.Tactic.Module.qNF.mkSubProof iR iM iRM t₁ t₂;
          q(⋯)
        else
          have pf := Mathlib.Tactic.Module.qNF.mkSubProof iR iM iRM (((a₁, x₁), k₁) ::ᵣ t₁) t₂;
          q(⋯)