TODO:
- "ncoercion" statement:
  - type processing to identify source/target
  - transitive closure (in the new Cic)
  - generation of hints to implement the pullback
- principles generation:
  - pretty printer for new statements required
- dependency graphs
- queries (on the trie?)
- serialization/undo
  - objects
  - ng_status (moo/lexicon)
- Tactics:
  - satuation
  - destruct

- Library.copy_at_level
- NCicRefiner.typeof e inferenza universi
- hints:
  - compare with the paper