X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FFsub%2Fpart1a.ma;h=55d97c266dd66395ef7c85c277df251e54e25d39;hb=55447138554f33c8588eb836d32ccce2402a09a3;hp=e12a64be4809093d647ba9f04a8906d42d2a9f83;hpb=247ec86cf6e8ba95843b408453afd57f7cf2d075;p=helm.git

diff --git a/helm/software/matita/library/Fsub/part1a.ma b/helm/software/matita/library/Fsub/part1a.ma
index e12a64be4..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.
 
 (* 
@@ -176,7 +176,7 @@ cut (\forall G,T,Q.(JSubtype G T Q) \to
                  |simplify;apply incl_nat_cons;assumption]]]
         |elim G2 0
            [simplify;unfold;intros;assumption
-           |intro;elim s 0;simplify;intros;apply incl_nat_cons;assumption]]]
+           |intro;elim t 0;simplify;intros;apply incl_nat_cons;assumption]]]
   |intros 4;(*generalize in match H1;*)elim H1
      [inversion H5
         [intros;rewrite < H8;apply (SA_Top ? ? H2 H3)