cons :: t → f → f
heightf :: f → N
heightt :: t → N
leaf :: t
max :: N → N → N
nil :: f
node :: f → t
s :: N → N
z :: N
heightf(nil) → z
heightf(cons(X, Y)) → max(heightt(X), heightf(Y))
heightt(leaf) → z
heightt(node(U)) → s(heightf(U))