----------------------------------------------------------------------
IS_EL_CONV                                                   (listLib)
----------------------------------------------------------------------
IS_EL_CONV : conv -> conv

SYNOPSIS
Computes by inference the result of testing whether a list contains a certain
element.

KEYWORDS
conversion, list.

DESCRIBE
{IS_EL_CONV} takes a conversion {conv} and a term {tm} in the following form:

   IS_EL x [x0;...xn]

It returns the theorem

   |- IS_EL x [x0;...xn] = F

if for every {xi} occurred in the list, {conv “x = xi”}
returns a theorem {|- P xi = F}, otherwise, if for at least one {xi},
evaluating {conv “P xi”} returns the theorem {|- P xi = T}, then it
returns the theorem

   |- IS_EL P [x0;...xn] = T


FAILURE
{IS_EL_CONV conv tm} fails if {tm} is not of the form described above, or
failure occurs when evaluating {conv “x = xi”} for some {xi}.

EXAMPLE
Evaluating

   IS_EL_CONV bool_EQ_CONV “IS_EL T [T;F;T]”;

returns the following theorem:

   |- IS_EL($= T)[F;F] = F




SEEALSO
listLib.SOME_EL_CONV, listLib.ALL_EL_CONV, listLib.FOLDL_CONV,
listLib.FOLDR_CONV, listLib.list_FOLD_CONV.

----------------------------------------------------------------------