simp [sliceL.aux, ByteArray.size, ih]
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 (aux acc (Nat.succ n✝) (head✝ :: tail✝)) = Array.size acc + Nat.succ n✝
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✝