proposition: Lemma functor_o a b c (g : {hom b, c}) (h : {hom a, b}) : F # [hom g \o h] = F # g \o F # h :> (el (F a) -> el (F c)).
proof: Proof. by rewrite functor_o_hom. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)