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