Simulation using WriterT Monad Transformers

Lemmas about simulateQ with output monad WriterT ω (OracleComp spec) for some ω

Note we only handle monoid version of WriterT, append should be added eventually.