GENLIST_CONV : conv -> conv
STRUCTURE
listLib
SYNOPSIS
Computes by inference the result of generating a list from a function.
DESCRIPTION
For an arbitrary function f, numeral constant n and conversion to evaluate f conv, the result of evaluating 
   GENLIST_CONV conv “GENLIST f n”
is the theorem 
   |- GENLIST f x = [x0;x1...xi...x(n-1)]
where each xi is the result of evaluating conv “f i”
EXAMPLE
Evaluating GENLIST_CONV BETA_CONV “GENLIST (\n . n) 4” will return the following theorem: 
   |- GENLIST (\n. n) 4 = [0; 1; 2; 3]

FAILURE
GENLIST_CONV tm fails if tm is not of the form described above, or if any call conv “f i” fails.
HOL  Kananaskis-11