Hola.
Se pueden usar cosas del Coq y en particular del manual, así se aprende.
No obstante, no se precisan arreglos en este ejercicio. Fijate como ir construyendo los árboles que aparecen en los ejemplos con emptyAB y addAB.
En particular, addAB podría ser:
Parameter addAB : forall n:nat, nat -> ABNat n -> ABNat n -> ABNat (n+1).
Saludos, Carlos