fix broken proofs in examples

[muenchnerkindl]

This is mostly housekeeping: fixing broken proofs in the examples contained in the distribution and making sure that the proofs of all theorems in the standard library work with the current version of the prover. There is also a change to theorem FS_Induction (in module library/FiniteSetTheorems.tla), intended to make that theorem easier to apply. This change breaks a few proofs in https://github.com/tlaplus/Examples, and I'll push a fix when this PR has been merged.

[ahelwer]

Ref #136; year and a half ago in that issue I made a list of the differences between the examples here and in the tlaplus/examples repo; I guess nothing really came of it but the proofs would be checked in CI if they were moved into the tlaplus/examples repo. That being said the proofs are also easy to check by adding to this repo's CI, the same as the library proofs in #218.

[muenchnerkindl]

Thanks @ahelwer! My take is that the mature proofs in the examples directory should indeed migrate to tlaplus/examples. Specifically, I removed the lamport-mutex proofs from tlapm/examples because it was a direct copy of the one in tlaplus/examples. I believe the same is true of the byzpaxos proofs and probably of some of the Bakery proofs, but I haven't really checked. Some of the other proofs are probably less interesting / less worked out and can remain here, IMHO. The other consolidation that needs to be done is about the Functions and SeqExtensions modules in tlapm/library vs. the Community modules, and I plan to address this as the next step.

[muenchnerkindl]

I'll merge this PR for now, then fix the affected proofs in tlaplus/examples, and finally align the example proofs here and in tlaplus/examples, based on @ahelwer's comparison.