fact: Definition flush_envT : envT Z M ~~> envT Z M := fun (X : UU0) t e => let: (x, _) := t e in (x, [::]).
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer imonad_model