proposition: Lemma transport_domF (a a' b : C) (p : a = a') (f : {hom a, b}) : transport_dom p f = [hom f \o hom_of_eq (esym p)].
proof: Proof. apply hom_ext; by subst a'. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)