Hola,
Tengo una duda sobre los nombres automáticos que Coq genera. Por ejemplo, si se usa "intros" sin nombrar las variables, Coq genera los nombres automáticamente.
La duda es cuánto se puede confiar en esos nombres en cuanto a la portabilidad. Es decir, ¿puede ocurrir que se generen nombres distintos según el entorno de desarrollo, versión de Coq, etc.? En el manual de referencia no encontré nada sobre el algoritmo de Coq para asignar los nombres.
Si bien hay formas de asignar manualmente los nombres, a veces prefiero no hacerlo porque hace menos legible a la prueba. Por ejemplo, tengo que hacer "intros a b c d n_le_m" para declarar la hipótesis "n_le_m", pero se que no voy a necesitar a, b, c ni d.
Saludos,
Nicolás