simp [*]
case base
α : Type
inst✝ : Ord α
n : Nat
first i j : Fin n
arr✝ : Vec α n
first✝ i✝ j✝ : Fin n
fi✝ : first✝ ≤ i✝
ij✝ : i✝ ≤ j✝
x✝ : ¬first✝ < i✝
⊢ (partitionImpl arr✝ first✝ i✝ j✝ fi✝ ij✝).snd[first✝] = arr✝[first✝]
no goals