PBETA_RULE : (thm -> thm)
STRUCTURE
SYNOPSIS
Beta-reduces all the paired beta-redexes in the conclusion of a theorem.
DESCRIPTION
When applied to a theorem A |- t, the inference rule PBETA_RULE beta-reduces all beta-redexes, at any depth, in the conclusion t. Variables are renamed where necessary to avoid free variable capture.
    A |- ....((\p. s1) s2)....
   ----------------------------  BETA_RULE
      A |- ....(s1[s2/p])....

FAILURE
Never fails, but will have no effect if there are no paired beta-redexes.
SEEALSO
HOL  Kananaskis-13