X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Falgebra%2Fmonoids.ma;h=63b6430ec90facf077bfbd3b4b346a9e124d7cc9;hb=35337934554027181913e87de11ff77745a77ebe;hp=fc6c8f956affc3a08edba8faeb6dd0f4de3ab23a;hpb=185bfc8f9c9ba49308477ee6769701f3e2977115;p=helm.git

diff --git a/helm/software/matita/library/algebra/monoids.ma b/helm/software/matita/library/algebra/monoids.ma
index fc6c8f956..63b6430ec 100644
--- a/helm/software/matita/library/algebra/monoids.ma
+++ b/helm/software/matita/library/algebra/monoids.ma
@@ -75,7 +75,7 @@ theorem is_left_inverse_to_is_right_inverse_to_eq:
  generalize in match (eq_f ? ? (λy.y·(r x)) ? ? H2);
  simplify; fold simplify (op M);
  intro; clear H2;
- generalize in match (associative ? (is_semi_group ? (monoid_properties M)));
+ generalize in match (op_associative ? (is_semi_group ? (monoid_properties M)));
  intro;
  rewrite > H2 in H3; clear H2;
  rewrite > H1 in H3;