Improved SPEC in order to take into account free variables of the theorem.