Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-12-19 16:15:23 -0800 (Mon, 19 Dec 2005)
Revision: 8323
Log message:

      Added rewrite bind_to_list_of_fun, which I believe is needed to prove
      bindn_to_list_of_fun. However, I don't know how to prove bind_to_list_of_fun
      -- I think we are missing a primitive rewrite like this or sth more basic.
      
      Now we should be able to prove bindn_to_list_of_fun by the handling of
      list_of_fun as Aleksey suggested in another thread.