auto and autogui... some work

[helm.git] / helm / software / matita / library / Fsub / part1a.ma

diff --git a/helm/software/matita/library/Fsub/part1a.ma b/helm/software/matita/library/Fsub/part1a.ma
index 795546299e842f8c2f2824a7c102db04e548d5d1..55d97c266dd66395ef7c85c277df251e54e25d39 100644 (file)
--- 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.
 
 (*