Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-14 17:07:24 -0800 (Sat, 14 Jan 2006)
Revision: 8479
Log message:

      Well, after much work, I'll probably need to take another approach
      to wf reasoning.
      
      Suppose we know
      
           sequent_bterm{"sequent"{arg; hyps; concl}} in BSequent
      
      where
           sequent_bterm is the Sequent -> BTerm{0} function
           BSequent is the type of well-formed BTerms than specify sequents
      
      What we would like is to know
           arg in BTerm{0}
           hyps in CVar{0}
           concl in BTerm{|hyps|}
      
      Of course, this is not true.  If the arg,hyps,concl are ill-formed,
      then we may get anything, even a BSequent.
      
      What we *do* know is that
      
           sequent_of_bterm{sequent_bterm{"sequent"{arg; hyps; concl}}} in Sequent
      
      However, sequent_of_bterm may return a sequent triple that is
      aribtrarily different from the triple (arg, hyps, concl).
      
      No idea what to do, thinking.