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