Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-18 18:27:04 -0800 (Sun, 18 Dec 2005)
Revision: 8317
Log message:

      Attempting the proof for TyAll{'ty1; x. 'ty2['x]}.
      
      This might be the challenge of a canonical form.
      The general goal is generalized eta-reduction.
      
         t in BTerm{'n +@ 1} -->
         bind{'n; x. bind{y. subst{substl{'t; 'x}; 'y}}}
         <-->
         t
      
      This individual theorem probably has an easy proof,
      and in general the concept seems obviously true.
      
      In the general case, there will be a stack of binds,
      usually of alternating vector/scalar form.
      
         bind{'n1; x1. bind{y1. bind{'n2; x2. bind{y1. ...}}}}}
      
      Let's see if we can prove it in general (not just
      this instance).
      
      Option 1:
         Do induction on 't.  Unfortunately, the bind-pushing
         tools in Itt_hoas_bterm_wf work only on concrete
         subterms lists.  Perhaps this can be generalized,
         but it is not obvious.
      
      Option 2:
         Prove a general bind-coalescing theorem, where we show
         that
            bind{'n; x. bind{y. ...}}
         turns into
            bind{'n +@ 1; x. ...}.
         See Itt_hoas_bterm_wf.coalesce_bindn_bind for a
         proof statement.
      
      Both options are not obvious at least to me.  Let's pose this as the
      immediate challenge.  Some immediate proposals that do not work:
      
         1. "I will tell Xin how to do it" (well, for Xin
            that is a good answer:)
         2. "You should write the subst{substl{...}}
             as substl{subst{...}}" (unless it can be shown
             how to write the conversion from one to the other).