# Main goals

- Fonctorise solver.ml with term module and theory module
- Add proof output

# Subgoals

- Move terms and theories to another directory (once fonctorised) ?