λA,B.λf: pre_magma_morphism A B. match f with [ mk_pre_magma_morphism f _ ⇒ f ].
ncoercion mmcarr: ∀A,B.∀M: pre_magma_morphism A B. A → B ≝ mmcarr
on _M: pre_magma_morphism ? ? to ∀_.?.
λA,B.λf: pre_magma_morphism A B. match f with [ mk_pre_magma_morphism f _ ⇒ f ].
ncoercion mmcarr: ∀A,B.∀M: pre_magma_morphism A B. A → B ≝ mmcarr
on _M: pre_magma_morphism ? ? to ∀_.?.