X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FFsub%2Fpart1a.ma;h=55d97c266dd66395ef7c85c277df251e54e25d39;hb=a180bddcd4a8f35de3d7292162ba05d0077723aa;hp=795546299e842f8c2f2824a7c102db04e548d5d1;hpb=cf4088e2cabcbce9b112f1e1fd5cfd38fe16d427;p=helm.git

diff --git a/helm/software/matita/library/Fsub/part1a.ma b/helm/software/matita/library/Fsub/part1a.ma
index 795546299..55d97c266 100644
--- a/helm/software/matita/library/Fsub/part1a.ma
+++ b/helm/software/matita/library/Fsub/part1a.ma
@@ -71,7 +71,7 @@ apply Typ_len_ind;intro;elim U
            |intros;destruct H10
            |intros;destruct H14
            |intros;destruct H14;rewrite > Hcut1;assumption]]
-     |split;unfold;intro;apply H5;apply natinG_or_inH_to_natinGH;auto]]
+     |split;unfold;intro;apply H5;apply natinG_or_inH_to_natinGH;autobatch]]
 qed.
 
 (*