have : as.size = as.pop.size + 1 := by
  rw [as.size_pop, Nat.sub_add_cancel (trans (r:=LE.le (α:=Nat)) (s:=LT.lt (α:=Nat)) k.zero_le h)]
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
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
this : size as = size (pop as) + 1
⊢ size (shrink.loop k (pop as)) = size as - Nat.succ k