Refactoring #4 #5
Description
PR #4 was merged under time pressure, and therefore several lemmas/definitions/tactics/etc are still "ad-hoc" and not moved to a proper loctation.
As part of this rewrite, we can also re-evaluate the overall library, and potentially refactor patterns shared in multiple "projects" (like Completeness or Tennenbaum) into common areas.
A first step is figuring out what should be moved.