...

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