Hola.
En el ej.20 los árboles binarios con completos. En el ej. 21 son árboles binarios comunes.
El lema del ej. 20 está bien planteado. No obstante, no veo la necesidad de usar max en la definición de ACom, ya que son árboles perfectos/completos:
constructor :forall (n:nat), A -> ACom n -> ACom n -> ACom (S n).
Saludos, Carlos