fact: Definition flush_stateT : stateT S M ~~> stateT S M := fun (X : UU0) t s => let: (x, _) := t s in (x, [::]).
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer imonad_model