(**********************************************************************)
TODO
+- elim_intros_simpl e rewrite[_back]_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