subst this
case base
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
h : ¬first < ↑last
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ ↑last
this : first = ↑last
⊢ (compare arr[i] arr[j]).isLE = true
case base
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
last i j : Fin n
ij : i ≤ j
jl : ↑j ≤ ↑last
h : ¬↑last < ↑last
fi : ↑last ≤ ↑i
⊢ (compare arr[i] arr[j]).isLE = true