case mk
val✝ : Fin size
⊢ SizeOf.sizeOf { val := val✝ } = toNat { val := val✝ } + 2
a : UInt64
⊢ SizeOf.sizeOf a = toNat a + 2
cases a
no goals
case mk
val✝ : Fin size
⊢ SizeOf.sizeOf { val := val✝ } = toNat { val := val✝ } + 2
simp_arith [UInt64.toNat]