(defstep exp2 ()
 (repeat (then 
	  (rewrite "exp2_def")
	  (rewrite "expt_inverse")
	  (rewrite "expt_plus")
	  (rewrite "expt_div" :dir RL)
	  (rewrite "expt_x1")
	  (rewrite "expt_x0")
	  (assert)))
 "exp2-catch-all-strategy, includes exp2_def expt_inverse expt_plus
 expt_div :dir RL expt_x1 expt_x0 and assert"
 "Rewriting with expt lemmas"
)

(defstep exp2prconst ()
 (then (expand "^")
  (apply (repeat (expand "expt"))))
 "Unrolls ^ (exponentiation)"
 "Unrolling ^"
)