Hola, no se como se aplica tauto a las definiciones de la 3.1.1.
Me podrían dar un ejemplo?
Por ejemplo para este:
Definition term_3_1_1 := fun (f: A -> A -> A) (t1: A) => t1.
Como se le aplica tauto y luego el exact?
Saludos
Lemma L1_tauto: (A -> A -> A) -> A -> A.
Proof.
tauto.
Qed.
Lemma L1_exact: (A -> A -> A) -> A -> A.
Proof.
intros f a; exact (f a a).
(* alternativamente: exact (fun (f:A->A->A) (a:A) => f a a). *)Qed.