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.
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.