proposition: Lemma fcomp_comp (A B C D : UU0) (f : A -> B) (g : C -> A) (m : D -> M C) : (f \o g) (o) m = f (o) (g (o) m).
proof: Proof. by rewrite 3!fcomp_def functor_o compA. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)