proposition: Lemma actm_comp A B C (g : B -> C) (h : A -> B) : actm (g \o h) = actm g \o actm h.
proof: Proof. by rewrite {1}/actm category.functor_o. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures) hierarchy