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