Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-02-20 21:40:19 -0800 (Mon, 20 Feb 2006)
Revision: 8752
Log message:

      I've been trying to prove a better elimination rule. I think provable_elim1
      better resembles what we need in pmn_core_terms. However, no matter how I tried,
      I always came across a well-formedness assumption (w: ty; ... => C[w] Type).
      
      So is the rule statement wrong? Or is this really what we need?