theorem ByteArray.append_array_data (a b : Array UInt8) : { data := a ++ b } = { data := a } ++ { data := b }

theorem ByteArray.push_size (b : ByteArray) (u : UInt8) : (b.push u).size = b.size + 1

theorem ByteArray.append_empty (b : ByteArray) : b ++ empty = b

theorem ByteArray.cons_eq_append (h : UInt8) (t : List UInt8) : { data := { toList := h :: t } } = { data := { toList := [h] } } ++ { data := { toList := t } }

theorem ByteArray.toList_loop_empty : toList.loop { data := { toList := [] } } 0 [] = []

theorem ByteArray.toList_empty : { data := { toList := [] } }.toList = []

theorem Array.extract_of_size_le {α : Type u_1} {as : Array α} {i j : ℕ} (h : as.size ≤ j) : as.extract i j = as.extract i

theorem List.loop_size_add (l : List UInt8) (b : ByteArray) : (toByteArray.loop l b).size = (toByteArray.loop l ByteArray.empty).size + b.size

theorem List.toByteArray_cons_size (h : UInt8) (t : List UInt8) : (h :: t).toByteArray.size = t.toByteArray.size + 1

theorem List.size_length_eq (l : List UInt8) : l.toByteArray.size = l.length

axiom Axioms.ByteArray.toList_eq (l : List UInt8) : { data := { toList := l } }.toList = l

This should be proved at some point