Got termination working.  Need to correctly insert ensures (see XXX in CPSConvert.hs).