transitivity (as.push bs[start])[as.size]
α : 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
hi : 0 < stop - start
ha : as.size + 0 < (foldl push as bs start stop).size
hb : start + 0 < bs.size
this : as.size + 0 < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[as.size + 0] = bs[start + 0]
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
hi : 0 < stop - start
ha : as.size + 0 < (foldl push as bs start stop).size
hb : start + 0 < bs.size
this : as.size + 0 < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[as.size + 0] = (as.push bs[start])[as.size]

case right
α : 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
hi : 0 < stop - start
ha : as.size + 0 < (foldl push as bs start stop).size
hb : start + 0 < bs.size
this : as.size + 0 < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (as.push bs[start])[as.size] = bs[start + 0]