IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Functionality Sequents and Well-formed Formulas - from Functions and Sequents
In Nuprl, the basic form for making assertions about the functional behavior of expressions with free variables is the Functionality Sequent, a special case of Sequents. In the degenerate form such assertions merely assert the well-formedness of expressions, indicating a type for the expression, such as " (x.x) " or " 1+2 {x:| 0<x }". (Note that an expression can have many types.)
More commonly, a sequent asserts the well-formedness of an expression in free variables or under assumptions. For example, the following sequent expresses the fact that "x+x" denotes a -valued function in x:
1. x : x+x
Or, considering a multi-argument function:
1. x : 2. y : x+x-(y+2)
Proofs of sequents often proceed by progressive decomposition of parts. See EXAMPLE
Equivalent assertions using closed forms for these function expressions would be these:
(x.x+x)
(x,y. x+x-(y+2))
For any type A, and any type-valued function B(x) over x A, the following assertions are equivalent:
(x.b(x)) x:AB(x)
1. x : A
b(x) B(x)
However, the sequent form generally is more expressive, because the sequent form
1. x : A
b(x) B(x)
means that
if the expression A denotes a type, then B(x) denotes a type-valued function over x A, and b(x) denotes a B(x)-valued function over A.
The purpose for this conditional is to allow us in proofs to separate the problem of showing that A denotes a type from the problem of showing other proof obligations. Suppose we want to show that " (x.b(x)) x:AB(x)". This can be broken into two independent problems of showing other sequents, namely,
The second of these assertions assumes for the sake of argument that A is a type, while the first of these assertions says that A is a type. Combining these justifies our original goal, namely, " (x.b(x)) x:AB(x)".
(
x.x) 
| 0<x }"
