A number of other logical concepts can be expressed in Nuprl. For example, the conditional and is sometimes used when dealing with partial functions. This connective can be defined as <p:prop> cand <q:prop> == (x:<p> # <q>). This results in an and connective which forces the evaluation of its first argument before the second argument.
As another example, sometimes it is useful to simplify the structure of a type considered as a proposition by ``squashing'' all of the proofs into one object. This squash operator is defined as
|| <p:prop> || == {0 in int | <p> }.
Thus if <p> is true then || <p> || consists of a single
object; all the different proofs have been identified. Note that this operator is
built using the subset type constructor.