fact: Definition handle_stateT (X : UU0) (t : stateT S M X) (h : unit -> stateT S M X) : stateT S M X := fun s => match t s with | inl z => h z s | inr x => inr x end.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer imonad_model