∀ {α : Type u_1} {n : ℕ} (lt : α → α → Bool) (lo hi : ℕ) (hhi : hi < n) (pivot : α)
  (_x :
    (_ : Vector α n) ×'
      (i : ℕ) ×'
        (k : ℕ) ×'
          (_ : autoParam (lo ≤ i) Array.qpartition._auto_2✝) ×'
            (_ : autoParam (i ≤ k) Array.qpartition._auto_4✝) ×' autoParam (k ≤ hi) Array.qpartition._auto_6✝),
  Array.qpartition.loop._unary✝ lt lo hi hhi pivot _x =
    PSigma.casesOn _x fun as i =>
      PSigma.casesOn i fun i k =>
        PSigma.casesOn k fun k ilo =>
          PSigma.casesOn ilo fun ilo ik =>
            PSigma.casesOn ik fun ik w =>
              if h : k < hi then
                if lt as[k] pivot = true then
                  Array.qpartition.loop._unary✝¹ lt lo hi hhi pivot ⟨as.swap i k ⋯ ⋯, ⟨i + 1, ⟨k + 1, ⟨⋯, ⟨⋯, ⋯⟩⟩⟩⟩⟩
                else Array.qpartition.loop._unary✝² lt lo hi hhi pivot ⟨as, ⟨i, ⟨k + 1, ⟨ilo, ⟨⋯, ⋯⟩⟩⟩⟩⟩
              else (⟨i, ⋯⟩, as.swap i hi ⋯ hhi)