proposition: Lemma pairhomK (f : {hom (x1,y1),(x2,y2)}) : pairhom (homfst f) (homsnd f) = f.
proof: Proof. apply/hom_ext/funext=> -[] i /=. by rewrite -homfstK. by rewrite -homsndK. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib category HB(structures)