The relevance list can be shorter than leftno (when the default is used).

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

diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma
index f72711aaab9d33880f00caf8b312d6a780e79121..1201c4fdf58a94c12aa1bb74579e354947100fea 100644 (file)
--- a/helm/software/matita/library/algebra/groups.ma
+++ b/helm/software/matita/library/algebra/groups.ma
@@ -264,7 +264,7 @@ apply H1;
 unfold member_of_subgroup;
 elim H2;
 apply (ex_intro ? ? (x'·a \sup -1));
-rewrite > f_morph;
+rewrite > f_morph; 
 apply (eq_op_x_y_op_z_y_to_eq ? (a \sub H));
 rewrite > (op_associative ? G);
 rewrite < H3;