Buenas, para probar el Lemma BorrarNoPertenece: forall (x:AB) (a:A), ~(Pertenece a (Borrar a x)).
habiendo definido Borrar usando Parameter eqGen: A->A->bool. en su definición, tuve que declarar un axioma que me permitiera razonar cuando sabemos si a = b. Por ejemplo, si tenemos a = b y eqGen a b = false, permite probar un absurdo. El axioma es Axiom eqGenEq: forall a b : A, a = b -> eqGen a b = true.
Es correcto esto? O debería poder escribir una prueba que no use el hecho de que si a = b entonces eqGen a b = true? Porque al menos como yo definí Pertence y Borrar (que es como entendí de la letra que habría que definirlas), en Pertenece estoy usando implícitamente esa igualdad propia de Coq (que deriva en las Props True o False), y en Borrar estoy usando un operador inventado eqGen que retorna un booleano, entiendo que si no explicito de alguna forma la relación entre ambos no sería posible razonar en base a la igualdad.
Gracias, saludos.