Buenas, llegue a algo así:
nat : Set
S : nat -> nat
a : nat
b : nat
c : nat
odd : nat -> Prop
even : nat -> Prop
P : nat -> Prop
Q : nat -> Prop
f : nat -> nat
x : nat
H : P x
---------------
P a
Y yo creo que eso es obvio, osea x es nat y se cumple P x entonces se cumple P a pero no se como cerrarlo.
No estoy seguro de lo que voy a decir pero creo que para demostrar P a, tendrías que tener algo del estilo "para todo x:nat, P x", no te basta saber que solo para x se cumple.
La respuesta es correcta.
El problema en la prueba planteada inicialmente entiendo viene por la elección de un testigo inadecuado en la prueba del existe.
Saludos, Carlos
Ok. Muchas gracias a ambos. Voy a buscar otra vuelta entonces, saludos.
