start removing our blessing from alt-ergo

[fdupress]

This is to remove our blessing from alt-ergo as a prover we wish all users to trust. In part also due to potential applications in non-open and commercial settings.

Individual researchers may still wish to trust it, but we aim to no longer require it for the stdlib and examples.

[fdupress]

There are three theories I expect to still fail:

• datatypes/Xreal
• theories/crypto/assumption/PKSMK
• theories/crypto/assumptions/DHIES

They all have two things in common: @bgregoir and a reading level beyond my Friday afternoon capabilities.

Benjamin, if you could attempt to make those three theories work without alt-ergo, that would be very kind.

[fdupress]

All stdlib should now be going through. I expect failures in the examples; which I'll tackle next.

Failures in the external CI should not be expected: they bring their own easycrypt.project, as intended. That being said, fixing the stdlib has involved adding a number of lemmas, so some SMT calls in external CI might lose stability.