; smme_mon : MonoidalEnrichment smme_e
; smme_mee : MonicMonoidalEnrichment _ smme_mon
}.
Coercion smme_e : SMME >-> Enrichment.
; smme_mon : MonoidalEnrichment smme_e
; smme_mee : MonicMonoidalEnrichment _ smme_mon
}.
Coercion smme_e : SMME >-> Enrichment.