SOME_EL_CONV : conv -> conv
STRUCTURE
listLib
SYNOPSIS
Computes by inference the result of applying a predicate to the elements of a list.
DESCRIPTION
SOME_EL_CONV takes a conversion conv and a term tm of the following form: 
   SOME_EL P [x0;...xn]
It returns the theorem 
   |- SOME_EL P [x0;...xn] = F
if for every xi occurred in the list, conv (--`P 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 
   |- SOME_EL P [x0;...xn] = T
FAILURE
SOME_EL_CONV conv tm fails if tm is not of the form described above, or failure occurs when evaluating conv (--`P xi`--) for some xi.
EXAMPLE
Evaluating 
   SOME_EL_CONV bool_EQ_CONV (--`SOME_EL ($= T) [T;F;T]`--);
returns the following theorem: 
   |- SOME_EL($= T)[T;F;T] = T
In general, if the predicate P is an explicit lambda abstraction (\x. P x), the conversion should be in the form 
   (BETA_CONV THENC conv')
SEEALSO
ALL_EL_CONV, IS_EL_CONV, FOLDL_CONV, FOLDR_CONV, list_FOLD_CONV
HOL  Kananaskis-10