From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 24 Mar 2010 17:48:45 +0000 (+0000)
Subject: Simplified proof after pattern fix
X-Git-Tag: make_still_working~2966
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b1736386d7728463cfcc7b3539633db9154809b5;p=helm.git

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 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;