----------------------------------------------------------------------
BUTFIRSTN_CONV                                               (listLib)
----------------------------------------------------------------------
BUTFIRSTN_CONV : conv

SYNOPSIS
Computes by inference the result of dropping the initial n elements of a list.

KEYWORDS
conversion, list.

DESCRIBE
For any object language list of the form {“[x0;...x(n-k);...;x(n-1)]”} ,
the result of evaluating

   BUTFIRSTN_CONV “BUTFIRSTN k [x0;...x(n-k);...;x(n-1)]”

is the theorem

   |- BUTFIRSTN k [x0;...;x(n-k);...;x(n-1)] = [x(n-k);...;x(n-1)]




FAILURE
{BUTFIRSTN_CONV tm} fails if {tm} is not of the form described above,
or {k} is greater than the length of the list.

----------------------------------------------------------------------