Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-09 14:30:17 -0800 (Mon, 09 Jan 2006)
Revision: 8435
Log message:

      Proved the initial set of simple theorems.
      
      The tactic will need some bind coalescing, and the routine stuff
      like eliminating mk_term, subst, bind.