-
Andrei Paskevich authored
Instead, we put a "stop_split" over the subsequent postcondition under the (begin > end + 1) assumption. When this assumption is unrealizable (strict for), this allows us to discharge the whole branch as a single goal.
fb77f394