no goals
α : Type u_1
as : List α
bs : Array α
⊢ Array.size (toArrayAux as bs) = length as + Array.size bs
induction as generalizing bs with
| nil => simp [toArrayAux]
| cons a as ih => simp_arith [toArrayAux, *]
no goals
case nil
α : Type u_1
bs : Array α
⊢ Array.size (toArrayAux [] bs) = length [] + Array.size bs
simp [toArrayAux]
no goals
case cons
α : Type u_1
a : α
as : List α
ih : ∀ (bs : Array α), Array.size (toArrayAux as bs) = length as + Array.size bs
bs : Array α
⊢ Array.size (toArrayAux (a :: as) bs) = length (a :: as) + Array.size bs
simp_arith [toArrayAux, *]