Coercion enr_c : Enrichment >-> ECategory.
(* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)
Coercion enr_c : Enrichment >-> ECategory.
(* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)