α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ 0 < sizeOf l
α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ sizeOf { fst := b, snd := a } < sizeOf (Lists'.cons' a l)
simp only [Sigma.mk.sizeOf_spec, Lists'.cons'.sizeOf_spec, lt_add_iff_pos_right]
no goals
α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ 0 < sizeOf l
apply sizeof_pos