case mk
val✝ : UInt32
valid✝ : UInt32.isValidChar val✝
⊢ SizeOf.sizeOf { val := val✝, valid := valid✝ } = toNat { val := val✝, valid := valid✝ } + 3
a : Char
⊢ SizeOf.sizeOf a = toNat a + 3
cases a
no goals
case mk
val✝ : UInt32
valid✝ : UInt32.isValidChar val✝
⊢ SizeOf.sizeOf { val := val✝, valid := valid✝ } = toNat { val := val✝, valid := valid✝ } + 3
simp_arith [Char.toNat]