eq moved to CProp

[helm.git] / helm / software / matita / nlibrary / algebra / magmas.ma

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index 0d4d7d6b10e06f689f271e612c9f3d1bc106a5b7..28b3795c88098743ba2648392ff77ef04c1244b1 100644 (file)
--- 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