proposition: Lemma bindmret (A : UU0) (m : failPState A) : bind m ret = m.
proof: Proof. apply: boolp.funext => s. unfold bind. destruct (m s) as [[|]]; reflexivity. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib monad_transformer