completed lemma 17

[helm.git] / helm / software / matita / nlibrary / PTS / subst.ma

diff --git a/helm/software/matita/nlibrary/PTS/subst.ma b/helm/software/matita/nlibrary/PTS/subst.ma
index a37074b4d306a60b85f7909bcecc2637b7849d82..77455d4cb848b8a097b2bb34926882820562ec86 100644 (file)
--- a/helm/software/matita/nlibrary/PTS/subst.ma
+++ b/helm/software/matita/nlibrary/PTS/subst.ma
@@ -107,7 +107,7 @@ napply (leb_elim (S n) k); nnormalize; #Hnk;
   ##[nrewrite > (le_to_leb_true ?? Hnk);nnormalize;//;
   ##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize;
       ##[nrewrite > (not_eq_to_eqb_false (n+1) k ?);
-         nnormalize;/2/; napply (not_to_not … Hnk);//;
+         nnormalize;/2/
       ##|napply le_S; napplyS (not_le_to_lt (S n) k Hnk);
       ##]
   ##]
@@ -178,7 +178,7 @@ ntheorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k →
   subst (lift B i (S k)) j A = (lift B i k).
 #A; #B; nelim B; nnormalize; /2/;
    ##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk;
-      napply eq_f2;/2/; napply Hind2;
+      napply eq_f2; /2/; napply Hind2;
       napplyS (monotonic_le_plus_l 1);//
    ##|#n; #i; #j; #k; #leij; #ltjk;
       napply (leb_elim (S n) i); nnormalize; #len;
@@ -211,7 +211,7 @@ nlemma subst_lemma: ∀A,B,C.∀k,i.
     ##[nrewrite > eqni; 
        nrewrite > (le_to_leb_true i (k+i) ?); //;
        nrewrite > (subst_rel2 …); nnormalize; 
-       napply symmetric_eq; 
+       napply sym_eq; 
        napplyS (lift_subst_ijk C B i k O);
     ##|napply (leb_elim (S (n-1)) (k+i)); #nk;
       ##[nrewrite > (subst_rel1 C (k+i) (n-1) nk);