Hola.
Parameter permite definir objetos de ciertos tipos, como axiomas esencialmente. Tal como vos decís, se está definiendo el tipo de add (y no su implementación) en:
Parameter add : forall n : nat, nat -> ArrayNat n -> ArrayNat (S n).
Respecto a "En los ejercicios que debemos definir los parámetros concat, zip, etc, la idea es solo definir su tipo?": SI. Por ejemplo:
Parameter concat : forall n m : nat, ArrayNat n -> ArrayNat m -> ArrayNat (n + m).
Respecto a tu última consulta de la parte 7, usá el tipo "bool" predefinido de Coq.
Saludos, Carlos