APPEND_CONV : conv
STRUCTURE
listLib
SYNOPSIS
Computes by inference the result of appending two object-language lists.
DESCRIPTION
For any pair of object language lists of the form --`[x1;...;xn]`-- and --`[y1;...;ym]`--, the result of evaluating 
   APPEND_CONV (--`APPEND [x1;...;xn] [y1;...;ym]`--)
is the theorem 
   |- APPEND [x1;...;xn] [y1;...;ym] = [x1;...;xn;y1;...;ym]
The length of either list (or both) may be 0.
FAILURE
APPEND_CONV tm fails if tm is not of the form --`APPEND l1 l2`--, where l1 and l2 are (possibly empty) object-language lists of the forms --`[x1;...;xn]`-- and --`[y1;...;ym]`--.
HOL  Kananaskis-10