proposition: Lemma hom_ext (C : category) (a b : C) (f g : {hom a, b}) : f = g <-> f = g :> (_ -> _).
proof: Proof. move: f g => [f [[Hf]]] [g [[Hg]]] /=; split => [[]//|fg /=]. rewrite fg in Hf Hg *. by rewrite (boolp.Prop_irrelevance Hf Hg). Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)