proposition: Lemma homfst_comp (x y z : A * B) (f : {hom x,y}) (g : {hom y,z}) : homfst [hom g \o f] = [hom homfst g \o homfst f].
proof: Proof. rewrite /homfst /=. case: cid => //= gh [gh1 gh2]. apply/hom_ext => /=. destruct g as [g [[g']]]. destruct f as [f [[f']]]. case: cid => g_ [g1 g2]. case: cid => f_ [f1 f2] /=. rewrite -ProductCategory.sepfst_comp. congr (ProductCategory.sepfst _ _). exact/proof_irr. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib category HB(structures)