Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-27 08:59:07 -0800 (Mon, 27 Mar 2006)
Revision: 8955
Log message:

      Proved a bunch of theorems about well-formedness of
      reflected terms.  This solves most of the intro proofs
      for elimination-style rules.  I'll finish it off soon.
      
      There were a couple of conflicts with .prla files.
      I've renamed my copies to .prla2.  I'll see what I can
      do to merge them.