fact: Definition local_stateT (f : Env -> Env) : stateT S M ~~> stateT S M := fun X t s e => t s (f e).
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer imonad_model