En la parte 4 pide remplazar los simbolos de interrogacion...
4. ([x:?]x [y:?]y)
para introducirlo en COQ lo pase a
Definition D324:=fun (x:A->B)=>fun(y:A)=>x y.
pero la verdad que no estoy seguro de que sea la intención del ejercicio?
Hola.
Está bien la idea aunque el término no es exactamente el indicado.
Ver:
Check ((fun x : (A -> B) -> A -> B => x) (fun y : A -> B => y)).
Saludos, Carlos
Ahora lo entendí...muchas gracias.