case mk
α : Sort u_1
p : α → Prop
val✝ : α
property✝ : p val✝
⊢ SizeOf.sizeOf { val := val✝, property := property✝ } = SizeOf.sizeOf { val := val✝, property := property✝ }.val + 1
α : Sort u_1
p : α → Prop
s : Subtype p
⊢ SizeOf.sizeOf s = SizeOf.sizeOf s.val + 1
cases s
no goals
case mk
α : Sort u_1
p : α → Prop
val✝ : α
property✝ : p val✝
⊢ SizeOf.sizeOf { val := val✝, property := property✝ } = SizeOf.sizeOf { val := val✝, property := property✝ }.val + 1
simp_arith