∀ {α : Type u_1} {n : ℕ} (as : Vector α n) (lo hi : ℕ) (w : autoParam (lo ≤ hi) Array.qsort._auto_2✝)
  (hlo : autoParam (lo < n) Array.qsort._auto_4✝) (hhi : autoParam (hi < n) Array.qsort._auto_6✝) (mid : ℕ)
  (hmid : lo ≤ mid ∧ mid ≤ hi) (as_1 : Vector α n) (h₂ : ¬mid ≥ hi),
  (invImage
        (fun x =>
          PSigma.casesOn x fun as lo =>
            PSigma.casesOn lo fun lo hi =>
              PSigma.casesOn hi fun hi w =>
                PSigma.casesOn w fun w hlo => PSigma.casesOn hlo fun hlo hhi => (hi, hi - lo))
        Prod.instWellFoundedRelation).1
    ⟨as_1, ⟨lo, ⟨mid, ⟨⋯, ⟨hlo, ⋯⟩⟩⟩⟩⟩ ⟨as, ⟨lo, ⟨hi, ⟨w, ⟨hlo, hhi⟩⟩⟩⟩⟩