fact: Definition runWriter : writer A -> pprod A W := unIdent ∘ (@runWriterT W Monoid_W ident A).
imports: ExtLib.Structures.Monads ExtLib.Structures.Monoid ExtLib.Data.PPair ExtLib.Data.Monads.IdentityMonad Coq.Program.Basics