proposition: Lemma pairhom_idfun : pairhom (a1:=a) (b1:=b) [hom idfun] [hom idfun] = [hom idfun].
proof: Proof. by apply/hom_ext/funext=> -[] x /=. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib category HB(structures)