Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-29 10:15:52 -0700 (Fri, 29 Oct 2004)
Revision: 6254
Log message:

      1.Added "nat{'n} in hyps" to ge_elim resource for Arith.
      2.As far as I understand indEquality was missing positivity hypothesis in the induction step subgoal.
      Luckily the proof didn't break when I've added that missing hyp.
      

Changes	Path
+5 -1	metaprl/theories/itt/itt_nat.ml
+861 -886	metaprl/theories/itt/itt_nat.prla