proposition: Lemma eq_bind (M : monad) (A B : UU0) (m : M A) (f1 f2 : A -> M B) : f1 =1 f2 -> m >>= f1 = m >>= f2.
proof: Proof. by move=> f12; congr bind; apply funext. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)