Hola Alfredo.
En el ejercicio 8:
Parameter ArrayNat : forall n:nat, Set.
el tipo de ArrayNat es nat -> Set. Esta definición nos permite definir un Set paramétrico en los naturales (arreglos de naturales de cierto largo).
Parameter add : forall n:nat, nat -> ArrayNat n -> ArrayNat (n + 1).
formaliza un operador que permite agregar un elemento de tipo nat a un arreglo de naturales de largo n, generando un arreglo de largo n+1.
Por ejemplo, un elemento de tipo ArrayNat 1 puede ser: add 0 8 empty. Esto es, un arreglo de largo 1 que tiene como único elemento al 8.
Con respecto a los ejercicios 13-15, solo se puede usar exact (no intros;exact). Tené en cuenta qué término permite construir un intro; por ejemplo analizá:
Lemma Ej: A -> A.
Proof.
exact (fun x : A => x).
Qed.
Saludos, Carlos