Beta : thm -> thm
STRUCTURE
Thm
SYNOPSIS
Perform one step of beta-reduction on the right hand side of an equational theorem.
DESCRIPTION
Beta performs a single beta-reduction step on the right-hand side of an equational theorem. 
   A |- t = ((\x.M) N)
  --------------------- Beta
   A |- t = M [N/x]

FAILURE
If the theorem is not an equation, or if the right hand side of the equation is not a beta-redex.
EXAMPLE
val th = REFL (Term `(K:'a ->'b->'a) x`);
> val th = |- K x = K x : thm

- SUBS_OCCS [([2],combinTheory.K_DEF)] th;
> val it = |- K x = (\x y. x) x : thm

- Beta it;
> val it = |- K x = (\y. x) : thm

COMMENTS
Beta is equivalent to RIGHT_BETA but faster.
SEEALSO
RIGHT_BETA, ETA_CONV
HOL  Kananaskis-10