More work on clocked big step semantics

The existing metatheory should all build again, and I've related the
clocked and unclocked big step semantics together.  I'm halfway through
proving totality for the clocked big step relation.