proposition: Lemma bindmret (A : UU0) (m : failPState A) : bind m ret = m.
proof: Proof. apply: funext => s. unfold bind. destruct (m s) as [[|]]; reflexivity. Qed.
imports: mathcomp(all_ssreflect) imonae_lib ihierarchy imonad_lib ifail_lib istate_lib imonad_transformer