- simple syntax
- generation of hints to implement the pullback
- principles generation:
- - projections for records
- induction/inversions
- dependency graphs
- queries (on the trie?)
BUGS:
----- 1) nwhd non fa nulla ??? OK, testa rigida
?2) cosa "corrisponde" alla simplify? multivm/breakpoint
=> la mu (+ iota) normalize
3) nelim bacata (assert ...), ma napply funziona