Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-07 20:07:12 -0800 (Mon, 07 Nov 2005)
Revision: 8128
Log message:

      Added a Boolean beq_bterm{'t1; 't2} for alpha-equality
      ('t1 = 't2 in BTerm <=> (beq_bterm{'t1; 't2} && 't1 in BTerm && 't2 in BTerm)).
      
      Also added the tactic (tailIndT << 'l >>) for tail induction on
      *any* list, not just the variables.  Bah, my proofs in Itt_list2
      would have been much easier if I had proved this first.