revert result
case base
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij✝ : i ≤ j
h : ¬first < i
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi ij✝ = result
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
case base
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij✝ : i ≤ j
h : ¬first < i
inv : LoopInvariant arr first i j last
⊢ ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
    partitionImpl arr first i j fi ij✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last