fact: Definition flush_exceptT (X : UU0) (t : exceptT Z M X) (h : Z -> exceptT Z M X) : exceptT Z M X := let: (c, _) := t in (c, [::]).
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer imonad_model