proposition: Lemma FCompE (C0 C1 C2 : category) (F : {functor C1 -> C2}) (G : {functor C0 -> C1}) a b (k : {hom a, b}) : (F \O G) # k = F # (G # k).
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)