Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-12-17 23:15:23 -0800 (Sat, 17 Dec 2005)
Revision: 8314
Log message:

      Another proof version for "reduce_vec_bind_of_mk_bterm_of_list_of_fun" in "t2".
      The idea is similar as Jason's, but a little simpler.