Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-08 15:23:45 -0800 (Tue, 08 Nov 2005)
Revision: 8140
Log message:

      This is like to be extremely contraversial.
      
      I added a "make_sequent" sequent, with an ML rewrite.
      
         make_sequent{'arg}{| x: Context{'e1}; y: Hypothesis{'e2['x]} >- 'concl['x; 'y] |}
      reduces to
         "sequent"{'arg;
             ['e1 @ [bind{length{'e1}; x. 'e2['x]}] @ nil]; 
             bind{length{'e1}; x. bind{y. 'concl['x; 'y]}}}
      
      My primary argument for doing so is that we want to reflect sequents as
      sequents, not something else.  However, since sequents are not primitive
      BTerms, and there are no induction forms defined for sequents in ITT,
      we have to do it primitively.  I realize this argument is not as
      strong as it should be.
      
      We need to be confident that this amounts to a definition.  I have not
      added the inverse rule because, among other things, it would have to
      be a conditional rewrite.
      
      This isn't just to make things pretty, I want to be able to use
      contexts in proofs.  For example, in Fsub, we would like a rule
      that looks as follows.
      
          Original FSub rule:
      
             <H>; x: ty1 >- e[x] in ty2 -->
             <H> >- lambda{x. e[x]} in TyFun{ty1; ty2} 
      
          Initial reflected version:
      
             <H1> >- 'H in CVar{0} -->
             <H1> >- 'ty1 in SOVar{|H|} -> ...
             <H1> >- Provable{make_sequent{| h: Context{'H}; x: Hypothesis{'ty1} >- e[x] in ty2|}} -->
             <H1> >- Provable{make_sequent{| h: Context{'H} >- lambda{x. e['x]} in TyFun{'ty1; 'ty2} |}
      
         Derived version:
             <H1> >- 'ty1 in SOVar{|H|} -> ...
             <H1> >- Provable{make_sequent{| h: <H>; x: Hypothesis{'ty1} >- e[x] in ty2|}} -->
             <H1> >- Provable{make_sequent{| h: <H> >- lambda{x. e['x]} in TyFun{'ty1; 'ty2} |}
      
      I admit, this "derived version" with real contexts may be a lost cause,
      but I'm not sure yet.