rw [toList1, List1.sizeOf_cons, ←sizeOf_toList, ih, Nat.add_left_comm]
case cons
α : Type u_1
β : Type ?u.12658
x : α
xs : List1.IndView α
ih : sizeOf xs.toList1 = 2 + sizeOf xs
⊢ sizeOf (cons x xs).toList1 = 2 + sizeOf (cons x xs)
case cons
α : Type u_1
β : Type ?u.12658
x : α
xs : List1.IndView α
ih : sizeOf xs.toList1 = 2 + sizeOf xs
⊢ 2 + (1 + sizeOf xs) = 2 + sizeOf (cons x xs)