(**********************************************************************)
TODO
+- assiomi
- Guardare il commento
(*CSC: this code is suspect and/or bugged: we try first without reduction
and then using whd. However, the saturate_term always tries with full