Buenas, en este ejercicio llegué 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
H1 : even a
H2 : forall x : nat, even x -> odd (S x)
______________________________________(1/1)
S a = b
No me doy cuenta como seguir a partir de aquí. Y en general no sé qué aplicar para demostrar a = b.
¿Alguna sugerencia?
Saludos, Hernán.