- compare with the paper
BUGS:
-
+1) la disambiguazione sembra generare termini (? ? ?) quando buca!
+ inoltre buca anche quando c'e' una scelta sola
?2) cosa "corrisponde" alla simplify? multivm/breakpoint
=> la mu (+ iota) normalize
-3) nelim bacata (assert ...), ma napply funziona
- prod_lemmas/symmetric_eqquadruple, napply (Prod4T ...)
-*4) nrewrite bacata, ma napply funziona
- freescale/bool_lemmas cercare !!!
*5) variabili libere => errore di tipaggio
6) sintassi per i NG naturali (serve una ndefault? serve una notazione