Entendí como crear los términos en COQ a partir del tipo. Pero tengo problema para escribir el termino fuera de COQ.
Estos dos ejercicios los trato de escribir y me quedan iguales pero no puede ser que el mismo termino corresponda a dos tipos diferentes.
(* λf.λt1.t1 *)
Definition term_teo1 := fun (f: A) (t1: B) => t1.
Check term_teo1. (* A -> B -> B *)
(* λf.λt1.t1 *)
Definition term_3_1_1 := fun (f: A -> A -> A) (t1: A) => t1.
Check term_3_1_1. (* (A -> A -> A) -> A -> A *)
Seguro el term_3_1_1 es el que esta mal la representación λf.λt1.t1.
Me pueden decir donde esta el error?
Saludos