Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-02-17 03:05:59 -0800 (Thu, 17 Feb 2005)
Revision: 6707
Log message:
Trying to prove "subst_commute".
Note: haven't fixed the broken proofs due to the additon of some rewrite conditions in Aleksey's last commit.