+ncoercion mmmcarr : ∀A,B,Ma,Mb.∀f: magma_morphism A B Ma Mb. pre_magma_morphism A B
+ ≝ mmmcarr
+ on _f: magma_morphism ???? to pre_magma_morphism ??.
+ndefinition mmcarr_mmmcarr ≝
+ λA,B,Ma,Mb.λf: magma_morphism A B Ma Mb. mmcarr ?? (mmmcarr ???? f).
+ncoercion mmcarr_mmmcarr : ∀A,B,Ma,Mb.∀f: magma_morphism A B Ma Mb. A → B ≝ mmcarr_mmmcarr
+ on _f: magma_morphism ???? to ∀_.?.