Some progress on a logical relation.

Doesn't do anything with modules or the store yet, and some reason HOL
isn't generating provable termination conditions in one case that should
be simple.