refactor: make the Std.Internal.Do loop invariant non-dependent

[sgraf812]

This PR makes the loop invariant of Std.Internal.Do a plain function of the elements consumed so far and the elements remaining, rather than a cursor indexed by the list being iterated. The for … invariant clause binds two lists, invariant pref suff => …, and verification conditions mention them directly instead of { prefix := …, suffix := …, property := ⋯ }.prefix.

Invariant xs β Pred := List.Cursor xs → β → Pred becomes Invariant α β Pred := List α → List α → β → Pred. The relation pref ++ suff = xs moves out of the type and into the hypotheses of the verification conditions, where it already appears. Dropping the index removes the List.Cursor.cast transports and the property proofs from the specification lemmas, and frees the forInWithInvariant gadgets from naming a list at all: taking inv : Invariant α β Pred, they no longer need the ForIn.toList bridge lemmas or the [ForIn Id ρ α] argument those required. RepeatInvariant, used for repeatM, was already non-dependent.

Std.Do is unchanged except for deleting List.Cursor.cast, which now has no use in either library.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5fe7f2454c32fe1605c6910f7140ce1f0a04f43b --onto 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-30 09:07:04)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-07-30 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-30 10:29:13)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2d0879c245c9804aafe2b9b52dde1eca0712f889 --onto 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-30 13:23:09)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5fe7f2454c32fe1605c6910f7140ce1f0a04f43b --onto a39eab69e1eee9ad38f4efe507907b1026a77808. You can force reference manual CI using the force-manual-ci label. (2026-07-30 09:07:06)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-07-30 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-07-30 10:29:15)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 2d0879c245c9804aafe2b9b52dde1eca0712f889 --onto a39eab69e1eee9ad38f4efe507907b1026a77808. You can force reference manual CI using the force-manual-ci label. (2026-07-30 13:23:11)