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-13