Remove custom SizeOf instances.

[abdoo8080]

Issue #, if available:

Description of changes:

This PR removes several custom SizeOf instances. The default instances provided by Lean interact much better with the built‑in termination checker, and the custom ones were interfering with automation.

Previously, a custom SizeOf String instance had been introduced to avoid non‑computability issues with the default instance. That workaround is not needed: the definition that depended on it now calls String.length directly, so the custom instance (which can break downstream code) is commented out.

Note: Many uses of @SizeOf.sizeOf α in the codebase are not guarded by an explicit [SizeOf α] argument, which causes Lean to fall back to the default instance and return 0 unexpectedly. Adding the missing type‑class arguments exposes further issues, since some types lack computable SizeOf instances. Long‑term, it may be cleaner to introduce a dedicated type-class and migrate the relevant code to use it consistently, rather than relying on Lean's automatically generated SizeOf instances.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.