fact: Definition evalStateT (N : monad) (S : UU0) (M : stateRunMonad S N) {A : UU0} (m : M A) (s : S) : N A := runStateT m s >>= fun x => Ret x.1.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib monad_transformer