proposition: Lemma bindmLfail (M : failR0Monad) S : BindLaws.right_zero (@bind (stateT S M)) (Lift _ _ ^~ fail).
proof: Proof. move=> A B m /=; rewrite /liftS/=; apply/funext => s; rewrite bindfailf. set x := (X in _ >>= X = _). rewrite (_ : x = fun=> fail) ?bindmfail//. by apply/funext=> -[b s']; rewrite /x/= bindfailf. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib