proposition: Lemma bindA (A B C : UU0) (m : failPState A) (f : A -> failPState B) (g : B -> failPState C) : bind (bind m f) g = bind m (fun x => bind (f x) g).
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