X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Falgebra%2Ffinite_groups.ma;h=766f9a6a73e457ae1d6e9630c9661b8bacec8eb5;hb=bfb7fbf61e86114e49cb3671503e8307a4582342;hp=0c7bd0b641914886a1ad659291da5b12eaff545c;hpb=af130d273b6be7fbcc2fb2504f3b28ef8fa2344f;p=helm.git

diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma
index 0c7bd0b64..766f9a6a7 100644
--- a/helm/software/matita/library/algebra/finite_groups.ma
+++ b/helm/software/matita/library/algebra/finite_groups.ma
@@ -93,6 +93,7 @@ elim n;
         [ simplify in H5;
           clear Hcut;
           clear Hcut1;
+          unfold f' in H5;
           clear f';
           elim H5;
           clear H5;
@@ -161,6 +162,7 @@ elim n;
         [ simplify in H5;
           clear Hcut;
           clear Hcut1;
+          unfold f' in H5;
           clear f';
           elim H5;
           clear H5;
@@ -395,6 +397,7 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
       assumption
     ]
   | intros;
+    unfold f;
     apply index_of_sur
   ] 
 ].