Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-22 15:39:54 -0800 (Thu, 22 Dec 2005)
Revision: 8345
Log message:

      - Added a "sqsimple" resource (with the term->bool output type) that can be
        used to tell whether an ITT type is squiggle-simple.
      
      - Added a sqsimple resource annotation processor that can be used to annotate
        rules of the form "sqsimple{nat}" and "sqsimple{A} --> sqsimple{A List}"
      
      - Changed the substT tactic to take advantage of the new sqsimple resource.
        Now when one runs something like "substT << a = b in (list{nat * int} + bool) >>,
        substT will know how to turn the equality into a squiggle one and do a
        substitution w/o generating any wf subgoals. hypSubstT and revHypSubstT will
        act similarly.