Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-04-04 23:39:42 -0700 (Tue, 04 Apr 2006)
Revision: 9022
Log message:

      Mostly proved subtyping is reflexive (Reflect_pmn_core_logic_test.intro_rule_test_ref); there are only a few well-formedness subgoals left unproven:
      
      /reflect_pmn_core_logic_test/intro_rule_test_ref/1/1/1/1/1/5
      /reflect_pmn_core_logic_test/intro_rule_test_ref/1/1/1/1/1/12
      /reflect_pmn_core_logic_test/intro_rule_test_ref/1/1/1/1/1/2/6/1
      /reflect_pmn_core_logic_test/intro_rule_test_ref/1/1/1/1/1/2/7/1
      
      -- They look hard to prove to me. Please take a look!