X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2FPTS%2Fgpts.ma;h=9af90225239158d425d63dd8cd90d8b2fbc2b1a7;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hp=d7fbe04403dc33f349268ab6ceb4186c3e395ba1;hpb=10e8d3c7da0978dd482e703004ced1138fdea8c0;p=helm.git

diff --git a/helm/software/matita/nlibrary/PTS/gpts.ma b/helm/software/matita/nlibrary/PTS/gpts.ma
index d7fbe0440..9af902252 100644
--- a/helm/software/matita/nlibrary/PTS/gpts.ma
+++ b/helm/software/matita/nlibrary/PTS/gpts.ma
@@ -198,15 +198,10 @@ ntheorem substitution_tj:
        napply (Hind2 ? (P::D));nnormalize;//;
     ##]
   ##|#G; #P; #Q; #R; #S; #tjP; #tjS; #Hind1; #Hind2;
-     #G1; #D; #N; #Heq; #tjN; nnormalize;
+     #G1; #D; #N; #Heq; #tjN; nnormalize in Hind1 ⊢ %;
      nrewrite > (plus_n_O (length ? D)) in ⊢ (? ? ? (? ? % ?));
-(*
-     napplyS (app (substl D N@G1) (subst P (length T D) N) A (subst R (length T D) N) (subst S (length T D) N) ?).
-     *)
-     nlapply (subst_lemma R S N (length ? D) 0); #sl;
-     nrewrite < (plus_n_O ?) in sl; #sl;
-     nrewrite > sl;
-     napply app; nnormalize in Hind1;/2/;
+     nrewrite > (subst_lemma R S N ? 0);
+     napplyS app; /2/;
   ##|#G; #P; #Q; #R; #i; #tjR; #tjProd; #Hind1; #Hind2;
      #G1; #D; #N; #Heq; #tjN; nnormalize;
      napplyS abs;