Sequents are introduced in Section 
.
We describe here some specific tactic-related details.
Hypotheses are conventionally numbered from left to right
,
starting from 1. These hypothesis numbers are displayed by the proof
editor, and tactics usually refer to hyps by these numbers.
Sometimes, it is convenient to consider the hyps numbered from right
to left
, and for this reason tactics consider a hyp list 
to also be numbered 
. Occasionally, the index
n+1 or 0 is used to refer to the hyp position to the right of the
last hyp.
There are tactics which work in similar ways on both hyps and the
concl. In this case, we call the hyps and concl collectively
clauses , refer to the concl as clause 0, and hyp i, 
as clause i. So far, we have not encountered tactics where
we would want to both refer to the position after the last hyp as clause
0 and refer to the conclusion, so this numbering scheme has not caused
problems.
When we want to indicate explicitly the number of a hyp in a schematic
sequent, we prefix the hyp with the number followed by a period. So
for example, if hyp i is proposition P, we write the hyp as 
.
Tactics currently use the visibility of the variable as an indication of whether it is ever used in subsequent hyps or the concl. Some tactics working on hyps are more efficient when they work on hyps whose variables are unused. The variables declared in a hypothesis list must all be distinct. Tactics are careful to use invisible variables for new hypotheses that are to be considered assumptions rather than declarations.