(**********************************************************************)
TODO
+- preoccupante: per
+ inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false).
+ noi generiamo anche i_rec e i_rect che Coq non genera (e che NON dovrebbero
+ essere accettati dal nostro nucleo che invece non fa una piega!!!)
- parsing contestuale (tattiche replace, change e forse altre)
- assiomi
- Guardare il commento