rw [Nat.succ_eq_add_one, Nat.add_assoc, Nat.add_comm 1 _]
case cons.succ
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n✝ : Nat
⊢ Array.size acc + 1 + n✝ = Array.size acc + Nat.succ n✝
no goals