The significance of the so--called judgements lies in the fact that they constitute the claims of a proof. They are the units of assertion ; they are the objects of inference. The judgements of have the form
where 
are distinct variables
and 
are terms (n may be 0),
every free variable of 
is one of 
,
and every free variable of S or of s is one of 
.
The list
is called the
hypothesis list or
assumption list, each 
:
is called a declaration
(of 
), each 
is called a hypothesis
or assumption , S is called
the consequent or conclusion ,
s the extract term (the reason will be seen later),
and the whole thing is called a sequent .
Before explaining the conditions which make a
sequent true
we shall define a relation 
, where H is a hypothesis list and
l is a list of terms,
and we shall define what it is for a sequent to be true at
a list of terms.
:
,
,
:
if and only if
*
*
& 
*
if 
We can also express this relation by saying that
every 
is a member of
and every 
is type --functional in
,
where 
means the set type
The sequent
is
true at 
if and only if
*
( 
*
& 
*
)
*
if 
:
,
,
:
*
& 
Equivalently, we can say that
s is S--functional in 
if
:
,
,
:
.
The sequent
is true if and only if
*
is
true at 
The connection between functionality and the truth of sequents lies in the
fact that S is type--functional (or s is S--functional) in 
if and only if T is a type and
for each member t of T, S is type--functional (s is S--functional)
in 
{x:T| x=t in T}.
Therefore, s is S--functional in 
if and only if T is a type and
the sequent x:T >> S [ext s] is true.
It is not always necessary to declare a variable with every hypothesis in a hypothesis list. If a declared variable does not occur free in the conclusion, extract term or any hypothesis, then the variable (and the colon following it) may be omitted.
In
it is not possible for the user to enter a complete
sequent directly; the extract term must be omitted.
In fact, a sequent is never displayed with its extract term.
The system has been designed so that upon completion of a proof,
the system automatically provides, or extracts, the extract term.
This is because in what is anticipated to be the standard mode of use,
the user tries to prove that a certain type is inhabited without
regard to the identity of any member.
One expects that in this mode the user thinks of the type
(that is to be shown inhabited) as a proposition, and that it
is merely the truth of this proposition that the user wants to show.
When one does wish to show explicitly that 
or that 
,
one instead shows the type (a = b in A) or the type
(a in A) to be inhabited.
Also, the system can often extract a term from an incomplete proof when the extraction is independent of the extract terms of any unproven claims within the proof body. Of course, such unproven claims may still contribute to the truth of the proof's main claim. For example, it is possible to provide an incomplete proof of the untrue sequent >> 1<1 [ext axiom], the extract term axiom being provided automatically.
Although the term extracted from a proof of a sequent is not displayed in the sequent, the term is accessible by other means through the name assigned to the proof in the user's library. It should be noted that in the current system proofs named in the user's library cannot be proofs of sequents with hypotheses.