exact as.getElem_pop i _
case succ
α : Type u
i k : Nat
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
IH : (shrink.loop k (pop as))[i] = (pop as)[i]
⊢ (pop as)[i] = as[i]
no goals