rw [foldl_stop] <;> try assumption
case refl
α : Type u_1
as bs : Array α
start : Nat
hstart : start ≤ start
hstop : start ≤ bs.size
⊢ (foldl push as bs start start).data = as.data ++ bs.data.extract start start
case refl
α : Type u_1
as bs : Array α
start : Nat
hstart : start ≤ start
hstop : start ≤ bs.size
⊢ as.data = as.data ++ bs.data.extract start start