rw [← as.push_pop_back' (hn ▸ n.zero_lt_succ)]
α : Type u
motive : Array α → Prop
empty : motive #[]
push : ∀ (as : Array α) (a : α), motive as → motive (Array.push as a)
n : Nat
IH : ∀ (as : Array α), size as = n → motive as
as : Array α
hn : size as = Nat.succ n
⊢ motive as
α : Type u
motive : Array α → Prop
empty : motive #[]
push : ∀ (as : Array α) (a : α), motive as → motive (Array.push as a)
n : Nat
IH : ∀ (as : Array α), size as = n → motive as
as : Array α
hn : size as = Nat.succ n
⊢ motive (Array.push (pop as) (back' as (_ : size as > 0)))