Boulmé

calling a FnMut from a closure

1

Hello, On this [file](https://github.com/xldenis/creusot/files/12861662/main.rs.gz), I got this error from Creusot: ``` cargo creusot -- --features=contracts -v Fresh autocfg v1.1.0 Fresh unicode-ident v1.0.12 Fresh cfg-if v1.0.0 Fresh proc-macro2 v1.0.69 Fresh num-traits...

Trivial intermediate assertions failed between two FnMut calls

9

Hello, The following code is proved with Creusot/Alt-Ergo. But if I decomment the two intermediate assertions on `a@`, they both fail (while everything else still works). This seems very weird...

The "apply" tactic generates an unexpected universe constraint (w.r.t. "refine")

4

### Description of the problem Below, in the "zarb" proof, if we use "apply eq_refl", the universe inference fails while typechecking the Goal at the end. If we replace "apply...