Better loop invariants

[W95Psp]

The design for loop invariant introduced by #857 (which will fix #605) is clunky:

• it works only for a very limited set of couple loops + iterators (see the documentation of hax_lib::loop_invariant)
• if the couple loop+iterator is not supported, there are no errors, it will produce bad code in the backend
• the ergonomics is bad:
  • the invariants are inside loops bodies, but none of the bindings introduced in the loops can be used
  • invariants are closure, and that's the responsibility of the user to annotate the type of the binder of that closure

We need something better:

• something that can work for any iterator, or at least for most of them, with a Rust error if that's the iterator is not supported
• closure should be typed automatically according to the context
• invariants should actually be before the loop, not inside