RIGHT_PBETA : (thm -> thm)
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Beta-reduces a top-level paired beta-redex on the right-hand side of an equation.
DESCRIPTION
When applied to an equational theorem, RIGHT_PBETA applies paired beta-reduction at top level to the right-hand side (only). Variables are renamed if necessary to avoid free variable capture. 
    A |- s = (\p. t1) t2
   ----------------------  RIGHT_PBETA
     A |- s = t1[t2/p]

FAILURE
Fails unless the theorem is equational, with its right-hand side being a top-level paired beta-redex.
SEEALSO
RIGHT_BETA, PBETA_CONV, PBETA_RULE, PBETA_TAC, RIGHT_LIST_PBETA, LEFT_PBETA, LEFT_LIST_PBETA
HOL  Trindemossen-1