From 3b6ca0e12de74ada4da4a3500a0cbffaa260c9e1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 6 May 2010 15:52:38 +0000 Subject: [PATCH] ... --- helm/software/matita/nlibrary/PTS/subst.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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); ##] ##] -- 2.39.2