Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-18 15:09:58 -0800 (Sun, 18 Dec 2005)
Revision: 8315
Log message:

      Added enough automation to prove that (TyTop in TyExp)
      is a well-formed proof rule.
      
      The list_of_fun theorem in Itt_hoas_debruijn was only the first
      step, because any actual term needs to have its subterms
      converted to list_of_fun form.  This raises the standard problem,
      that the length{...} term is stated in dependent form, though
      we know that it is ultimately independent.
      
      Here are the steps to prove a wf goal of the form
      
         bind{.... mk_term{op; [s1; ...; sn]}} in BTerm{...}
      
         1. First, convert the subterm list to a vlist{| s1; ...; sn |}.
            The vlist{| ... |} form is nice because it is always
            a list, no matter what the elements are.  These vector
            form are somewhere in between a variable and an actual
            concrete list.
      
            Proved various lemmas like:
               length{vlist{| <J[x]> |}} <--> length{vlist{| <J[it]> |}}
      
         2. Defined a subterms_bind{bind{...; terms}} term that is used
            to push the binds into the list.
      
         3. Defined a tactic bindWFT to perform all the steps in the
            wf reasoning.
      
      Problems:
         I don't know why, but adding the bindWFT tactic to autoT does not
         work.  We get some strange things like.
      
            dT 0 thenT autoT  (* completely proves the goal *)
         but
            autoT (* does nothing... *)
      
         I am not sure of all the strategies in autoT, but it seems
         to me that adding something to "intro" should have some effect
         on autoT...
      
      The final tactic then is:
      
         let proofRuleWFT = repeatT (autoT thenT tryT bindWFT thenT rw reduceC 0)