Hola.
1- Si, en el término addA el n es el que determina el largo del array. Pero en el tipo sobra un n; debería ser: addA : forall n:nat, nat -> ArrayNat n -> ArrayNat (S n).
2- Por ahora estamos viendo los tipos definidos como decís, pero en el siguiente módulo definiremos, por ejemplo, los array como un tipo inductivo con constructores empty y add. Veremos luego que esto tiene diferencias, ya que será posible tener esquemas de inducción y recursión asociados a los tipos inductivos. Al definir tipos y operadores con Parameter (como en este práctico) no estamos diciendo cosas que si es posible con definiciones inductivas, por ejemplo que todos los array se generan solo con empty y add.
Saludos, Carlos