Scripts fixed. They were broken since the change to the behaviour of CicMetaSubst...

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

diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma
index 0c7bd0b641914886a1ad659291da5b12eaff545c..766f9a6a73e457ae1d6e9630c9661b8bacec8eb5 100644 (file)
--- 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
   ] 
 ].