fact: Definition product_action (m12 : M12) (x12:X12) := ⟨nfst m12 ⧕ nfst x12, nsnd m12 ⧕ nsnd x12⟩.
imports: Coq(ssreflect ssrfun ssrbool List) Coq(FunctionalExtensionality) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures)