0 :: d
cons :: d → c → c
false :: a
height :: d → d
if :: a → d → d
le :: d → d → a
map :: (d → d) → c → c
maxlist :: d → c → d
nil :: c
node :: b → c → d
s :: d → d
true :: a
map(F, nil) → nil
map(Z, cons(U, V)) → cons(Z(U), map(Z, V))
le(0, W) → true
le(s(P), 0) → false
le(s(X1), s(Y1)) → le(X1, Y1)
maxlist(U1, cons(V1, W1)) → if(le(U1, V1), maxlist(V1, W1))
maxlist(P1, nil) → P1
height(node(X2, Y2)) → s(maxlist(0, map(height, Y2)))