-notation < "M" for @{ 'semigroup $M }.
-interpretation "premonoid coercion" 'premonoid M =
- (cic:/matita/algebra/monoids/premonoid.con M).
-
-notation < "M" for @{ 'typeofmonoid $M }.
-interpretation "premonoid coercion" 'typeofmonoid M =
- (cic:/matita/algebra/monoids/Type_of_Monoid.con M).
-
-notation < "M" for @{ 'magmaofmonoid $M }.
-interpretation "premonoid coercion" 'magmaofmonoid M =
- (cic:/matita/algebra/monoids/Magma_of_Monoid.con M).
-