intro i k hk hi
α : Type u
as : Array α
⊢ ∀ (i k : Nat) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
α : Type u
as : Array α
i k : Nat
hk : k ≤ size as
hi : i < size as - k
⊢ (shrink.loop k as)[i] = as[i]