[ bugfix ] Finished fixing the proofs

Yesterday I removed a useless datatype and today I finished fixing
the proofs which used to depend on it. The main impact is that their
are quite a lot less proofs.
Also, I've refactored some of them in order to have something a bit
better behaved.