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])....