proposition: Lemma homfstK (x y : A * B) (f : {hom x,y}) (i : el x.1) : inl (homfst f i) = f (inl 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)