Simplified proof after pattern fix

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

diff --git a/helm/software/matita/nlibrary/PTS/gpts.ma b/helm/software/matita/nlibrary/PTS/gpts.ma
index d7fbe04403dc33f349268ab6ceb4186c3e395ba1..9af90225239158d425d63dd8cd90d8b2fbc2b1a7 100644 (file)
--- 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;