congr 1
case left
α : Type u_1
as bs : Array α
start stop i✝ : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝¹ : start < bs.size
i : Nat
hi : i + 1 < stop - start
ha : as.size + (i + 1) < (foldl push as bs start stop).size
hb : start + (i + 1) < bs.size
this✝ : as.size + (i + 1) < (foldl push (as.push bs[start]) bs (start + 1) stop).size
this : (as.push bs[start]).size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[as.size + (i + 1)] =
    (foldl push (as.push bs[start]) bs (start + 1) stop)[(as.push bs[start]).size + i]
case left.e_i
α : Type u_1
as bs : Array α
start stop i✝ : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝¹ : start < bs.size
i : Nat
hi : i + 1 < stop - start
ha : as.size + (i + 1) < (foldl push as bs start stop).size
hb : start + (i + 1) < bs.size
this✝ : as.size + (i + 1) < (foldl push (as.push bs[start]) bs (start + 1) stop).size
this : (as.push bs[start]).size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ as.size + (i + 1) = (as.push bs[start]).size + i