huge update. compiles.  rewriting engine.  general properness proofs are admitted, but general equational reasoning is working with heavy automation support.  up next: implementing monad transformers and showing they maintain galois connections.