exact this ▸ inv
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
this : i = first
⊢ LoopInvariant arr first first j last
no goals