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.

[atomb]

I agree. Have you tried adding those constraints to see if anything breaks? If it works without requiring substantial changes I'd love to include that change in this PR.

[abdoo8080]

Yes. I can add [SizeOf P.Ident] [SizeOf P.Ty] [SizeOf P.Expr] to Cmd.sizeOf, but it doesn't actually change anything: the function is never called. Since all custom SizeOf instances in Strata have been removed, Lean now uses the elaborator‑generated instance instead. I can delete Cmd.sizeOf entirely if you prefer. Note that I can't do the same for Stmt.sizeOf and Block.sizeOf functions. Adding SizeOf constraints to them causes non-computability errors in Strata/Core's partial evaluator. As I mentioned in the PR description, the cleanest solution is to introduce a dedicated type-class to compute the size of a program and migrate the relevant code to use it consistently, rather than relying on the SizeOf type-class.