BETAS_CONV : conv

SYNOPSIS
Beta conversion over multiple arguments.

DESCRIPTION
Given a term t of the form `(\x1 ... xn. t[x1,...,xn]) s1 ... sn`, the call BETAS_CONV t returns
  |- (\x1 ... xn. t[x1,...,xn]) s1 ... sn = t[s1,...,sn]

FAILURE CONDITIONS
Fails if the term is not of the form shown, for some n.

EXAMPLE
  # BETAS_CONV `(\x y. x + y) 1 2`;;
  val it : thm = |- (\x y. x + y) 1 2 = 1 + 2

SEE ALSO
BETA_CONV, RIGHT_BETAS.