proposition: Lemma bindE (a b : C) (f : {hom a, F b}) (m : el (F a)) : bind f m = join b (([the {functor C -> C} of F] # f) m).
proof: Proof. rewrite /join /=. rewrite /=bind_fmap/idfun/=. congr (fun f => bind f m). by rewrite hom_ext. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)