Finished one lemma (after many bug fixes here and there).

[helm.git] / matita / library / algebra / monoids.ma

diff --git a/matita/library/algebra/monoids.ma b/matita/library/algebra/monoids.ma
index fc6c8f956affc3a08edba8faeb6dd0f4de3ab23a..63b6430ec90facf077bfbd3b4b346a9e124d7cc9 100644 (file)
--- a/matita/library/algebra/monoids.ma
+++ b/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;