fact: Definition strict_list_monoid : monoid := strict_monoid (listMonoid O).
imports: Coq(ssreflect ssrfun ssrbool List) Coq(FunctionalExtensionality) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures)