Several fixes and refinements
Began work on Conduit.v, just missing monad_law_1