Hola, tengo una duda.
En este ejercicio a la familia de arboles binarios de altura n (AB) lo defini con dos constructores. Uno para el caso en que el subárbol derecho tiene mayor altura y otro para el izquierdo.
Inductive AB (A:Set) : nat->Set:=
emptyAB : AB A 0
| addABi :forall ni nd :nat, A-> AB A ni->AB A nd-> AB A (S ni)
| addABd : forall ni nd :nat, A-> AB A ni->AB A nd-> AB A (S nd).
pero me queda la duda si esos dos constructores no se unifican en uno que la altura sea la máxima de ambos subárboles.
Algo asi como:
addABd:forall ni nd :nat, A-> AB A ni->AB A nd-> AB A (S (max ni nd)).
Muchas gracias