induction xs with
| pure x => rw [toList1]; rfl
| cons x xs ih => rw [toList1, List1.sizeOf_cons, ←sizeOf_toList, ih, Nat.add_left_comm]; rfl
α : Type u_1
β : Type ?u.12658
xs : List1.IndView α
⊢ sizeOf xs.toList1 = 2 + sizeOf xs
no goals