Hola.
Las rotaciones no son relevantes aquí, ya que nos enfocamos solo en la propiedad estructural de los AVL, que establece que para cada nodo las alturas de sus subárboles izquierdo y derecho pueden diferir en a lo sumo una unidad.
Para árboles AVL no vacíos se podrían definir tres operadores, tendiendo en cuenta que las alturas de los subárboles de un nodo pueden ser iguales o diferir en una unidad. Por ejemplo, uno de estos operadores puede ser:
Parameter addAVL1 : forall n:nat, nat -> AVLNat n -> AVLNat (n+1) -> AVLNat (n+2).
Saludos, Carlos