Practico 3.1.3

Re: Practico 3.1.3

de Carlos Luna -
Número de respuestas: 0

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.