proposition: Lemma homsnd_idfun x : homsnd (x:=x) [hom idfun] = [hom idfun].
proof: Proof. apply/hom_ext; rewrite boolp.funeqE => x1 /=. case: cid => i [i1 i2] /=. rewrite (_ : i = ProductCategory.idfun_separated _)//. by rewrite ProductCategory.sepsnd_idfun. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib category HB(structures)