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.