Minimize dependencies from `Anneal.lean`, generated Lean

Currently, we depend on all of `Aeneas` in `Anneal.lean`, leading to multi-second import times from `lake build`. Instead, we should:
- Minimize these imports
- Refactor `Anneal.lean` so that it contains distinct modules which only depend narrowly on the parts of `Aeneas` which they need
- Provide this library as an *external* dependency (perhaps installed via `cargo anneal setup`?) and, in generated Lean, only import the needed modules (and allow users to import more for their own annotations)