EL_CONV : conv
STRUCTURE
SYNOPSIS
Computes by inference the result of indexing an element from a list.
DESCRIPTION
For any object language list of the form --`[x0;...xk;...;xn]`-- , the result of evaluating
   EL_CONV (--`EL k [x0;...xk;...;xn]`--)
is the theorem
   |- EL k [x0;...;xk;...;xn] = xk

FAILURE
EL_CONV tm fails if tm is not of the form described above, or k is not less than the length of the list.
SEEALSO
HOL  Kananaskis-10