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:
Identify (and document!) the main theorems relating the various semantics and correctness of the well-formedness checker.
Write a script to search backwards and find all definitions that are still used
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: