Hola Damián.
No entiendo en qué contexto tenés n=m para esta prueba. No obstante, según lo que describís, si en tu goal aparece G(S n) y tenés en tus hipótesis n=m, aplicas rewrite.
Si querés enviame tu prueba y veo bien lo que decís, ya que quizás te referís al axioma inj, que no se precisa en este ejercicio.
No obstante, no está mal usar cut, generando pasos/resultados intermedios en una prueba.
Saludos, Carlos