(**********************************************************************)
TODO
+- LApply deve prendere in input gli identificatori che va a generare;
+ lascio a Ferruccio la scelta della sintassi concreta
- elim_intros_simpl e rewrite[_back]_simpl: ora non viene usata dal
^^^^^^ ^^^^^^
toplevel la variante che semplifica. Capire quali sono i problemi