Refine does beta-reductions.

To avoid the unpleasantness of having beta-redex in terms after an application of refine, refine is followed by lazy beta.