cases heq
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ (foldl push as bs start stop).data = as.data ++ bs.data.extract start stop
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