X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Falgebra%2Fmagmas.ma;h=f7757ba096a0d76ad62d625bd720567821b4a8dd;hb=47f4d2af2a592e2e6c0e0ea5f90ffae2fbf6391a;hp=e49d8ea82545549e7b9c3818f1ba029879ede330;hpb=9f8544610ba0245bde47f367de6716e1f256ab18;p=helm.git

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index e49d8ea82..f7757ba09 100644
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -58,10 +58,6 @@ ndefinition mmmcarr ≝
 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 ∀_.?.
 ndefinition mmclosed ≝
  λA,B,Ma,Mb.λf: magma_morphism A B Ma Mb.
   match f return λf: magma_morphism A B Ma Mb.∀x. x ∈ Ma → f x ∈ Mb with