Hola.
Lo que se pide inicialmente es dar términos de los tipos indicados. Por ejemplo:
Variable A B C : Set.
(*1*)
Definition Ej1_1_a_1 (f : A -> A -> A) (x : A) := f x x.
Definition Ej1_1_a_2 (f : A -> A -> A) (x : A) := x.
(* 2 *)
Usando Check se pueden ver que ambos términos tienen el mismo tipo (son dos habitantes del mismo tipo):
Check Ej1_1_a_1.
Check Ej1_1_a_2.
(*3*)
La parte 3 para el ejemplo de arriba sería:
Lemma Ej1_3_a_1 : (A -> A -> A) -> A -> A.
Proof.
tauto.
Qed.
Lemma Ej1_3_a_2 : (A -> A -> A) -> A -> A.
Proof.
intros H H0; exact (H H0 H0).
Qed.
Saludos, Carlos