Remove all obvious dead code and unused lemmas

[dgarbuzov]

Grepping the source reveals that there are many lemmas whose identifiers only appear once, in the definition. There is probably a lot of dead code not related to the semantics still in the repository. We should:

1. Identify (and document!) the main theorems relating the various semantics and correctness of the well-formedness checker.
2. Write a script to search backwards and find all definitions that are still used
3. GC