Buenas, a mí no me termina de quedar claro bien cómo utilizar el tema de los subsets. Estuve leyendo la documentación y la verdad siempre me termino perdiendo.
Entiendo que por ejemplo sig sería equivalente a forall x:A, P x ->sig A P pero no me doy cuenta como usarlo. Por ejemplo, en el caso del ejercicio 1 que se tiene:
Lemma predspec : forall n : nat, {m : nat | n = 0 /\ m = 0 \/ n = S m}.
Yo si asumo que es un exists y me defino una variable de tipo nat puedo hacer exists variable y como que me voy metiendo en la prueba. El tema es que no sé si está bien hacer eso (tuve que declarar una variable), dos tampoco me salió por ahí y tres no use nada de sig.
Me doy cuenta que es el mismo problema que cuando quise encarar el ejercicio 6.2, pero no sé si estoy mirando algo mal o que, pero no me logro dar cuenta.
Saludos y muchas gracias.