+- elim_intros_simpl e rewrite_simpl: ora non viene usata dal
+ ^^^^^^ ^^^^^^
+ toplevel la variante che semplifica. Capire quali sono i problemi
+ e/o cosa fare delle varianti con semplificazione.
+- eta_expand non usata da nessuno?
+- eliminare eta_fix? (aspettare notazione da Zack e Luca)
+- bug di ferruccio: fare un refresh dei nomi dopo l'applicazione
+ di una tattica. Di quali nomi fare refresh? (Andrea) di quelli
+ veramente ambigui, ovvero dell'ultimo binder tale che sotto di
+ esso un nome viene usato in maniera ambigua. Esempio:
+ \lambda x. \lambda x. (x x) (dove una x e' -2) ==> fare refresh
+ \lambda x. \lambda x. (x x) (dove entrambe sono -1) ==> non fare refresh
+- a volte genera termini con variabili legate da piu' binder
+ Capita quando un tipo dall'environment (e.g. \lambda x.T)
+ viene inserito in un contesto (e.g. x:nat) dove le variabili
+ sono gia' state legate in precedenza.