dsimp [shrink] at hi ⊢
α : Type u
as : Array α
n : Nat
h : n ≤ size as
i : Nat
hi : i < size (shrink as n)
⊢ (shrink as n)[i] = as[i]
α : Type u
as : Array α
n : Nat
h : n ≤ size as
i : Nat
hi : i < size (shrink.loop (size as - n) as)
⊢ (shrink.loop (size as - n) as)[i] = as[i]