Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-20 15:49:14 -0800 (Fri, 20 Jan 2006)
Revision: 8540
Log message:

      Proved 0 <--> 1, thus demonstrating that
      Meta_context_terms.reduce_sequent_ind_base1 is way too strong!
      
      # pwd ()
      /itt_vector/itt_vec_list1/bug : string
      # ls ""
      
      * <*>
      ....main....
      <Γ> Ã¢ÂŠÂ¢ 0 Ã¢Â‰Â¡ 1
      
      BY [...]
      
      # check ()
      The proof of /itt_vec_list1/bug depends on the following definitions and axioms:
              Definition /meta_context_terms2/unfold_sequent_ind_uv
              Conditional Rewrite /meta_context_terms/reduce_sequent_ind_base1
              Rewrite /base_meta/reduce_meta_sum
              Rewrite /itt_int_base/reduce_add_meta
              Rewrite /itt_int_base/reduce_numeral
              Rewrite /itt_vec_list1/unfold_vlist_nest
              Rewrite /meta_context_terms/reduce_hbeta
              Rewrite /meta_context_terms/reduce_sequent_ind_base2
              Rewrite /meta_context_terms/reduce_sequent_ind_left
              Rule /base_rewrite/rewriteAxiom1
              Rule /itt_equal/equalityAxiom
              Rule /itt_squiggle/squiggleHypSubstitution
              Rule /itt_squiggle/squiggleRef
              Rule /itt_struct/cut
              Rule /itt_struct/introduction
              Rule /itt_struct/thin_many