X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2FPTS%2Fsubst.ma;h=77455d4cb848b8a097b2bb34926882820562ec86;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=5282e86baa5465c7e14e4eccaadd99dcf80b1eb6;hpb=10e8d3c7da0978dd482e703004ced1138fdea8c0;p=helm.git

diff --git a/helm/software/matita/nlibrary/PTS/subst.ma b/helm/software/matita/nlibrary/PTS/subst.ma
index 5282e86ba..77455d4cb 100644
--- 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);
       ##]
   ##]