Hola
Siguiendo este hilo, la igualdad entre elementos de un tipo A podría ser un parámetro de la relación inductiva sobre listas que lo usa (similar al ejemplo de sorted).
Sin usar la igualdad, una opción alternativa para definir una relación inductiva es usar el mismo elemento (variable) en cada instancia correspondiente a la definición, como se muesta en un mensaje de este hilo para la igualdad entre listas, por ejemplo.
Saludos Carlos
Siguiendo este hilo, la igualdad entre elementos de un tipo A podría ser un parámetro de la relación inductiva sobre listas que lo usa (similar al ejemplo de sorted).
Sin usar la igualdad, una opción alternativa para definir una relación inductiva es usar el mismo elemento (variable) en cada instancia correspondiente a la definición, como se muesta en un mensaje de este hilo para la igualdad entre listas, por ejemplo.
Saludos Carlos