simp [quickSort', h]
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : n > 0
⊢ sortedRange (quickSort' arr) 0 (n - 1)
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : n > 0
⊢ sortedRange (quickSortImpl arr 0 ⟨n - 1, ⋯⟩) 0 (n - 1)