# We can bring together two proofs or programs, using "and"
# on the propositions we have proved.  So far we don't
# have proof of much.

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

# Here, the term of interest is & & &, with type (&True&True&).
# The term is a tuple containing two subterms, each of type True,
# and each consisting of the space (optional) between a pair of &'s.