@[simp]

theorem Fin.sizeOf {n : Nat} (a : Fin n) : sizeOf a = ↑a + 1

@[simp]

theorem BitVec.sizeOf {w : Nat} (a : BitVec w) : sizeOf a = sizeOf a.toFin + 1

@[simp]

theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 3

@[simp]

theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 3

@[simp]

theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 3

@[simp]

theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 3

@[simp]

theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 3

@[simp]

theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 4

@[simp]

theorem Subtype.sizeOf {α : Sort u_1} {p : α → Prop} (s : Subtype p) : sizeOf s = sizeOf s.val + 1