Buenas tardes,
Si bien creemos entender el ejercicio, estamos teniendo problemas para encontrar la correcta sintaxis reconocida en coq para representar por ejemplo:
λx.x:A->A ?
Muchas gracias.
Saludos.
Hola.
En Coq λ es fun. La identidad puede expresarse entonces con la definición:
Definition id : A -> A :=
fun x => x.
Saludos, Carlos
Ah! Genial!
Muchas gracias!