simp only [autoParam] at h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : autoParam (i < (foldl push as bs start stop).size) _auto✝
⊢ (foldl push as bs start stop)[i] = as[i]
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
⊢ (foldl push as bs start stop)[i] = as[i]