Evaluate the list reversal function applied to a specific list.
DESCRIPTION
When applied to a term `REVERSE [t1; ...; tn]` with a concrete list (though
not necessarily with constant or ground elements) the conversion REVERSE_CONV
returns the appropriate theorem |- REVERSE [t1; ...; tn] = [tn; ...; t1].
FAILURE CONDITIONS
Fails if the term is not of the expected form.
EXAMPLE
# REVERSE_CONV `REVERSE [1;2;3]`;;
val it : thm = |- REVERSE [1; 2; 3] = [3; 2; 1]
# REVERSE_CONV `REVERSE [one;two;three]`;;
val it : thm = |- REVERSE [one; two; three] = [three; two; one]