case mk
α : Type u_1
inst✝ : SizeOf α
fn✝ : Unit → α
⊢ sizeOf { fn := fn✝ } = 1 + sizeOf (Thunk.get { fn := fn✝ })
α : Type u_1
inst✝ : SizeOf α
a : Thunk α
⊢ sizeOf a = 1 + sizeOf (Thunk.get a)
cases a
no goals
case mk
α : Type u_1
inst✝ : SizeOf α
fn✝ : Unit → α
⊢ sizeOf { fn := fn✝ } = 1 + sizeOf (Thunk.get { fn := fn✝ })
rfl