case mk
n val✝ : Nat
isLt✝ : val✝ < n
⊢ SizeOf.sizeOf { val := val✝, isLt := isLt✝ } = { val := val✝, isLt := isLt✝ }.val + 1
n : Nat
a : Fin n
⊢ SizeOf.sizeOf a = a.val + 1
cases a
no goals
case mk
n val✝ : Nat
isLt✝ : val✝ < n
⊢ SizeOf.sizeOf { val := val✝, isLt := isLt✝ } = { val := val✝, isLt := isLt✝ }.val + 1
simp_arith