Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-31 17:02:29 -0800 (Fri, 31 Mar 2006)
Revision: 8980
Log message:

      Added some forward rules. Now the test rule in "pmn_core_terms_test" is almost proved except for the "base_theory" subgoal.
      
      However, I do not know how to prove sequent_bterm_forward0, which basically states that "sequent_bterm{s} in BTerm" implies "s in Sequent".