proposition: Lemma bindLfailf (M : failMonad) S : BindLaws.left_zero (@bind (stateT S M)) (Lift _ _ ^~ fail).
proof: Proof. move=> A B g /=; rewrite /liftS; apply: boolp.funext => s; rewrite bindfailf. set x := (X in X >>= _ = _). by rewrite (_ : x = fail) ?bindfailf// /x bindfailf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib state_lib