proposition: Lemma functorcomposition_comp : FunctorLaws.comp functorcomposition.
proof: Proof. by move=> a b c g h; rewrite /functorcomposition; rewrite 2!functor_o_hom. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)