remove alt-ergo from EasyCrypt TCB

[fdupress]

This makes stdlib and examples go through without alt-ergo, and removes
that prover from the expected set of provers for EC CI.

This makes EasyCrypt more cleanly usable in commercial and non-free
contexts. Our docker images still contain alt-ergo versions, which are
available for proofs in external CI and individual proofs, upon a user's
(hopefully informed) choice.

Anyone wanting to transition their proofs away from alt-ergo should
expect proofs that use SMT to solve goals that require either
instantiation of existentials or case analysis on inductively-typed
values to fail after removing alt-ergo.

[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.

[vbgl]

I’ve pushed two commits that are relevant to this PR in an other branch: vbgl@d89de85

They fix the proofs of the examples without alt-ergo.

[fdupress]

Thanks, I'm not at work today, but if @strub or @Cameron-Low are able to cherry-pick those over to check CI, that would be grand.

@vbgl, tell Benjamin he owes you a bunch for those proofs.

[strub]

@fdupress I let you do the final cleaning & squashing. But everything seems OK now.

[strub]

Fix the added FIXME: cleanup

[fdupress]

Cleaned up, squashed, and expanded a bit on the commit message. — Please check, @strub.