Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-26 12:22:49 -0800 (Sun, 26 Feb 2006)
Revision: 8786
Log message:

      - Allow nth_hyp annotations on forward-chaining rules that do not have wf
        subgoals.
      
      - Added nth_hyp annotations on bunch of forward-chaining rules in HOAS theory
      
      - Proved several rules like "t in BSequent --> t in BTerm" and added them to
        nth_hyp.