Small changes here and there. Changed Coq code from verbatim to
lhs2tex stuff.