Buenas,
Realizando el ejercicio 1 del práctico 3 me surgieron algunas dudas.
En la primera parte del ejercicio no me queda claro cómo saber si un elemento está en beta forma normal. Por ejemplo, para el tercer tipo (A -> B) -> (A -> B -> C) -> A -> C, se me ocurrieron dos "habitantes" distintos:
Definition term3_1 := fun (f: A -> B) (g: A -> B -> C) (a: A) => g a (f a).
Definition term3_2 := fun (f: A -> B) (g: A -> B -> C) => (fun (a: A) => g a (f a)).
Ambos tienen el tipo pedido (verificado usando Check), pero no sé darme cuenta de cuál(es) está(n) en beta forma normal. También me queda la duda de si es correcto usar "fun", vi que en otros ejercicios del práctico no se usa.
En la parte 3 de este mismo ejercicio, me quedán 2 dudas. La primera es qué significa que un tipo sea una tautología (es decir, por ejemplo para el tipo mencionado previamente, pude demostrar Theorem tauto3: (A -> B) -> (A -> B -> C) -> A -> C., pero no entiendo qué significa esto). También me queda la duda de si en la parte de realizar la prueba utilizando exact, solo se puede usar esa táctica, o si además se pueden usar otras como intros.
Gracias y saludos
Eliana