Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-10 01:04:26 -0800 (Fri, 10 Feb 2006)
Revision: 8660
Log message:

      Turns out that we do not really need the "weak reverse functionality" axiom
        list{'A} Type --> nil in list{'A} and it sufficient to have
        list{'A} --> nil in list{'A} in nthHypT.
      
      The latter form is actually derivable, so I was able to get rid of the only
      remaining prim rule in itt_list. Now itt_list is truly derived!