LEFT_PBETA
PairRules.LEFT_PBETA : (thm -> thm)
Beta-reduces a top-level paired beta-redex on the left-hand side of an equation.
When applied to an equational theorem, LEFT_PBETA applies paired
beta-reduction at top level to the left-hand side (only). Variables are
renamed if necessary to avoid free variable capture.
A |- (\x. t1) t2 = s
---------------------- LEFT_PBETA
A |- t1[t2/x] = s
Failure
Fails unless the theorem is equational, with its left-hand side being a top-level paired beta-redex.
See also
Drule.RIGHT_BETA,
PairRules.PBETA_CONV,
PairRules.PBETA_RULE,
PairRules.PBETA_TAC,
PairRules.RIGHT_PBETA,
PairRules.RIGHT_LIST_PBETA,
PairRules.LEFT_LIST_PBETA