proposition: Lemma FCompA (F : {functor C2 -> C3}) (G : {functor C1 -> C2}) (H : {functor C0 -> C1}) : (F \O G) \O H = F \O (G \O H).
proof: Proof. apply: functor_ext=> *; by rewrite FCompE. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)