New reduction strategy (that behaves much better during simplification).

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

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index a9164a927bde9cf2f937d77a2b8f0dabadd64428..9d98aea4d9d232758c1145db350da6a78f71d3a6 100644 (file)
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -49,15 +49,10 @@ intros;
 unfold left_cancellable;
 intros;
 rewrite < (e_is_left_unit ? ? (monoid_properties G));
-fold simplify (e G);
 rewrite < (e_is_left_unit ? ? (monoid_properties G) z);
-fold simplify (e G);
 rewrite < (opp_is_left_inverse ? ? (group_properties G) x);
-fold simplify (opp G);
 rewrite > (semigroup_properties G);
-fold simplify (op G);
 rewrite > (semigroup_properties G);
-fold simplify (op G);
 apply eq_f;
 assumption.
 qed.