simp [sliceL.aux]
case cons.zero
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
⊢ Array.size (aux acc Nat.zero (head✝ :: tail✝)) = Array.size acc + Nat.zero
no goals