PBETA_RULE
PairRules.PBETA_RULE : (thm -> thm)
Beta-reduces all the paired beta-redexes in the conclusion of a theorem.
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.
See also
Conv.BETA_RULE,
PairRules.PBETA_CONV,
PairRules.PBETA_TAC,
PairRules.RIGHT_PBETA,
PairRules.LEFT_PBETA