proposition: Lemma homsndK (x y : A * B) (f : {hom x,y}) (i : el x.2) : inr (homsnd f i) = f (inr i).
proof: Proof. case: f=> /= f [[Hf]]. case: cid => -[sf1 sf2] [Hf1 Hf2] /=. by case: cid => j ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib category HB(structures)