proposition: Lemma bindLmfail (M := [the monad of option_monad]) S T U (m : stateT S M U) (FAIL := @throw unit T tt) : m >> Lift [the monadT of stateT S] M T FAIL = Lift [the monadT of stateT S] M T FAIL.
proof: Proof. rewrite /= /liftS; apply: boolp.funext => s. rewrite except_bindE. rewrite {1}bindE /= MS_mapE {1}/bindS /=. by case (m s) => // -[]. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib monad_transformer monad_model