[eacsl] Use `toplevel_predicate` in `Translate.translate_predicate`

The function `Translate.translate_predicate` is meant to translate the
root predicate of an assertion, so it makes sense to use
`toplevel_predicate` as a parameter and it gives access to the
`predicate_kind`.

The loop invariants in `Env` are also stored as `toplevel_predicate`
to facilitate the translation.