BUTLAST_CONV : conv
STRUCTURE
listLib
SYNOPSIS
Computes by inference the result of stripping the last element of a list.
DESCRIPTION
For any object language list of the form --`[x0;...x(n-1)]`-- , the result of evaluating 
   BUTLAST_CONV (--`BUTLAST [x0;...;x(n-1)]`--)
is the theorem 
   |- BUTLAST [x0;...;x(n-1)] = [x0;...; x(n-2)]

FAILURE
BUTLAST_CONV tm fails if tm is an empty list.
HOL  Kananaskis-10