refactor: state `while` loop invariants over an exit flag (#14845)

This PR gives the invariant of a `while` or `repeat` loop its own type,
`def Std.WP.WhileInvariant α Pred := Bool → α → Pred`, a predicate over
the loop's `exit` flag and the loop state. Previously, it reused
`Std.WP.RepeatInvariant α α Pred = α ⊕ α → Pred`, a type which is
awkward to use in practice.