En el ejercicio se pide probar que la relación provista es de equivalencia. Mirando la forma en la que se estructura, cumple la definición de relación de equivalencia, pero no entiendo bien qué es lo que hay que probar con Coq.
¿Cuál es la idea del ejercicio?
Muchas gracias!