LEFT_LIST_PBETA : (thm -> thm)
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Iteratively beta-reduces a top-level paired beta-redex on the left-hand side of an equation.
DESCRIPTION
When applied to an equational theorem, LEFT_LIST_PBETA applies paired beta-reduction over a top-level chain of beta-redexes to the left-hand side (only). Variables are renamed if necessary to avoid free variable capture. 
    A |- (\p1...pn. t) q1 ... qn = s
   ----------------------------------  LEFT_LIST_BETA
       A |- t[q1/p1]...[qn/pn] = s

FAILURE
Fails unless the theorem is equational, with its left-hand side being a top-level paired beta-redex.
SEEALSO
RIGHT_LIST_BETA, PBETA_CONV, PBETA_RULE, PBETA_TAC, LIST_PBETA_CONV, LEFT_PBETA, RIGHT_PBETA, RIGHT_LIST_PBETA
HOL  Kananaskis-13