open `Lean.Loop` / `repeat` and `while` notation to proofs

Stream: lean4

[Robin Arnez]

The repeat and while notations currently make it impossible to prove things about them, due to working with the opaque Lean.Loop.forIn. However, it is possible (for most monads) to write a definition of Lean.Loop.forIn that works with an equality theorem

forIn l init f =
  f () init >>= fun
    | .done val => pure val
    | .yield val => forIn l val f

Here is a proof of concept of how such an integration would go:
Loop.lean
(this one uses partial_fixpoint to make things simpler, so you need a newer version of lean, e.g. nightly)
(the proof on the bottom is an example of it working with a complex monad, although there probably should be more simp lemmas or lawful classes that would make the proof less painful)
The point of this would be to make it more possible to use monadic notation and in particular repeat and while with proofs. There is definitely a lot to do still to make monadic implementations better to work with but I think this would be a good step.