let sorted := quickSort' ⟨arr, rfl⟩
α : Type
inst✝ : Order α
arr : Array α
⊢ (quickSort arr).size = arr.size
α : Type
inst✝ : Order α
arr : Array α
sorted : Vec α arr.size := quickSort' ⟨arr, ⋯⟩
⊢ (quickSort arr).size = arr.size