clear h n
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ ∀ (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]