induction k generalizing as with
| zero => rfl
| succ k IH =>
  dsimp [shrink.loop]
  specialize IH as.pop (as.size_pop ▸ Nat.le_sub_of_add_le hk) (by rewrite [as.size_pop, Nat.sub_sub, Nat.add_comm]; exact hi)
  rewrite [IH]
  exact as.getElem_pop i _
α : Type u
as : Array α
i k : Nat
hk : k ≤ size as
hi : i < size as - k
⊢ (shrink.loop k as)[i] = as[i]
no goals