RIGHT_LIST_BETA : (thm -> thm)
STRUCTURE
Drule
SYNOPSIS
Iteratively beta-reduces a top-level beta-redex on the right-hand side of an equation.
DESCRIPTION
When applied to an equational theorem, RIGHT_LIST_BETA applies beta-reduction over a top-level chain of beta-redexes to the right hand side (only). Variables are renamed if necessary to avoid free variable capture. 
    A |- s = (\x1...xn. t) t1 ... tn
   ----------------------------------  RIGHT_LIST_BETA
       A |- s = t[t1/x1]...[tn/xn]

FAILURE
Fails unless the theorem is equational, with its right-hand side being a top-level beta-redex.
SEEALSO
BETA_CONV, BETA_RULE, BETA_TAC, LIST_BETA_CONV, RIGHT_BETA
HOL  Kananaskis-13