have : as.size + i < (foldl push (as.push bs[start]) bs (start+1) stop).size := by
  rw [size_append_aux (start+1) stop (Nat.succ_le_of_lt hstart') hstop]
  rw [size_push]
  rw [Nat.add_assoc]
  apply Nat.add_lt_add_left
  rw [Nat.add_comm]
  rw [Nat.sub_succ']
  rw [Nat.sub_add_cancel]
  exact hi
  rw [Nat.le_sub_iff_add_le hstart]
  rw [Nat.add_comm]
  exact Nat.succ_le_of_lt hstart'
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : as.size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]