refactor: clean up the Std.Internal.Do weakest-precondition library

This PR refactors the internal `Std.Internal.Do` specification library. The weakest-precondition application lemmas are renamed to follow the naming convention: the transformer lemmas `<T>.apply_wp` become `<T>.wp_apply_eq`, and the `WPMonad.<op>_<inst>_wp` family becomes `WPMonad.wp_<op>_<inst>_apply_eq` when the conclusion is an equality and `WPMonad.le_wp_<op>_<inst>_apply` when it is an entailment. The `Triple` entailment field is renamed from `rel_wp` to `le_wp`. The loop-invariant types `Invariant`, `StringInvariant`, and `StringSliceInvariant` take their cursor and accumulator arguments curried rather than as a single tuple.

The precondition-generic monad spec lemmas (`Spec.pure'`, `Spec.bind'`, `Spec.map'`, `Spec.seq'`) are removed in favour of the `Triple` rules: `Triple.map` and `Triple.seq` are added alongside the existing `Triple.pure` and `Triple.bind`, and the `@[spec]` lemmas `Spec.pure`/`bind`/`map`/`seq` derive from them.

It also adds supporting `Prop`- and function-lattice order lemmas (`le_of_right`, `le_of_imp_top_le`, `true_le_of_top_le`, `le_of_forall_le`, `top_le_of_forall_top_le`), `while`-loop specifications (`WhileInvariant`, `WhileVariant`, `Spec.whileM`, `Spec.forIn_loop`), and the early-return invariant combinators `Invariant.withEarlyReturnNewDo`, `StringInvariant.withEarlyReturnNewDo`, and `StringSliceInvariant.withEarlyReturnNewDo`.

Co-authored-by: volodeyka <vovaglad00@gmail.com>