IS_EL_CONV : conv -> conv
STRUCTURE
listLib
SYNOPSIS
Computes by inference the result of testing whether a list contains a certain element.
DESCRIPTION
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
SOME_EL_CONV, ALL_EL_CONV, FOLDL_CONV, FOLDR_CONV, list_FOLD_CONV
HOL  Kananaskis-13