@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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