# Here's a slightly more interesting type, but the use
# of False means that you wouldn't expect a useful proof
# or program.

((& & hang &:(&True&False&)) be (\@b->b))

# This program hangs.  You wouldn't expect to be able to prove True and False.