proposition: Lemma eq_bind {A B} (m : M A) : forall (f1 f2 : A -> M B), (forall a, f1 a = f2 a) -> bind m f1 = bind m f2.
proof: Proof. move=> ? ? /functional_extensionality -> //. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures MonadExamples SpecificationMonads DijkstraMonadExamples) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)