BUTFIRSTN_CONV : conv
STRUCTURE
listLib
SYNOPSIS
Computes by inference the result of dropping the initial n elements of a list.
DESCRIPTION
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.
HOL  Kananaskis-10