2 - "ncoercion" statement:
3 - type processing to identify source/target
4 - transitive closure (in the new Cic)
5 - generation of hints to implement the pullback
6 - principles generation:
7 - pretty printer for new statements required
9 - queries (on the trie?)
12 - ng_status (moo/lexicon)
17 - Library.copy_at_level
18 - NCicRefiner.typeof e inferenza universi
20 - compare with the paper