Brief tutorial on how to write a progress and preservation proof for
small-step semantics in Twelf.