X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Falgebra%2Fmagmas.ma;h=28b3795c88098743ba2648392ff77ef04c1244b1;hb=28da21926eb9cab187ba8a64999c760083f60369;hp=0d4d7d6b10e06f689f271e612c9f3d1bc106a5b7;hpb=a17430d258e886b5164fca3d65ee7da7c40e6a36;p=helm.git

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index 0d4d7d6b1..28b3795c8 100644
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -71,5 +71,6 @@ ndefinition mm_image:
   | #x; #y; *; #x0; #Hx0; *; #y0; #Hy0; nwhd;
     napply (ex_intro ????)
      [ napply (op ? x0 y0) 
-     | nelim daemon ]##]
+     | napply (conj ????);
+       nelim daemon ]##]
 nqed.
\ No newline at end of file