Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-16 20:05:43 -0800 (Fri, 16 Dec 2005)
Revision: 8312
Log message:

      I was curious, so I tried the approach that Aleksey suggested.
      As you might guess, it worked, and it was pretty easy:b  This is in
      Itt_hoas_debruijn.reduce_vec_bind_of_mk_bterm_of_list_of_fun (sorry
      about the long name, I was dubious at the time).
      
      It would be nice to see a shorter proof than mine (19 ruleboxes).
      Perhaps one of you (including the Aleksey oracle) can do better?
      
      Sorry I suggested a simple (though non-obvious to me) theorem.  However,
      I am sure I will once again be flabbergasted, and soon enough we will come
      up with a nontrivial example that will strain/elucidate the heuristic.
      
      ---- Aside ----
      
      Itt_vec_sequent_term is another example of the heuristic, where the
      destructor part (the "length" term) is not originally in non-dependent
      form.  However, it can be proved that the dependent form is equivalent
      to a non-dependent form.  Basically, it works like this:
      
      1. Prove that the destructor does not depend on the binders.
      
         For some interesting terms "e":
      
         bind{<H> >- e[length{'x}] }
         <-->
         bind{<H> >- e[length{bind{<H> >- 'x}}]}
      
      2. Hoist the closed destructor <<length{bind{<H> >- 'x}}>>.
      
      3. Now work hard for a while, and you are done.