Nadrieril

@bors r+

I'm working onremoving the need for `rustup`

Btw, rustup should no longer be needed

Actually, why not add `charon` to the dev shell? You'd have to find a way to male `charon-ml` available to opam. The idea being that someone who only wants to...

Oh you're right, I was thinking of aeneas devs but this PR is for aeneas users. Nevermind

Oh yeah this needs latest charon; I'll bump soon

We can likely replace all `Copy` bounds with `Clone` bounds, but is that an improvement? Your type signature would stay roughly the same

Maybe a `--discard-unused-bounds` flag on Charon would make sense, under which we could often remove the `Copy` bounds altogether

Or normalization could just ignore those builtins, so that you can further normalize it later with a different implementation that does support the builtin ? Not a common usecase though.

Noting here that I no longer think we need the "`&` everywhere" part of the proposal. This makes the proposed fix less local but saves us in design and possible...