Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-08 23:41:52 -0800 (Wed, 08 Dec 2004)
Revision: 6348
Log message:

      Removed the wf hypothesis from the bterm_elim2 rule. Xin, I am leaving the
      bterm_elim2 and bterm_elim3 to you.
      

Changes	Path
+4 -2	metaprl/theories/itt/itt_reflection.ml
+3393 -3258	metaprl/theories/itt/itt_reflection.prla
+8 -3	metaprl/theories/itt/itt_struct2.ml