Sobre la (No)Aplicabilidad de un Teorema de Modelo Pequeño a la Comprobación de Modelos STM