rw [toList1]
case pure
α : Type u_1
β : Type ?u.12658
x : α
⊢ sizeOf (pure x).toList1 = 2 + sizeOf (pure x)
case pure
α : Type u_1
β : Type ?u.12658
x : α
⊢ sizeOf (List1.cons x []) = 2 + sizeOf (pure x)