This PR verifies the `String.Slice.splitToSubslice` function by relating
it to a model implementation `Model.split` based on a
`ForwardPatternModel`.
The proof is generic, so it works for splitting by characters, strings
etc.
From this, we will be able to give user-facing API lemmas for
`String.split` and friends in future PRs.
We also move the verification of string patterns from
`String.Slice.Pattern` to `String.Slice.Pattern.Model` to achieve better
separation between code that users run in their programs and code that
only supports the theory.
6f51ec27ed