From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 Jun 2005 08:51:48 +0000 (+0000)
Subject: Removed a dummy "let ... in" that was there only to show a bug (now fixed).
X-Git-Tag: INDEXING_NO_PROOFS~12
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=feac5909f11bc7cf2e2d57f4bb7a5729784be483;p=helm.git

Removed a dummy "let ... in" that was there only to show a bug (now fixed).
---

diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma
index a28afef87..27e51e69c 100644
--- a/helm/matita/tests/fguidi.ma
+++ b/helm/matita/tests/fguidi.ma
@@ -89,9 +89,8 @@ theorem le_gen_S_S_cc: \forall m,n. (le m n) \to (le (S m) (S n)).
 intros. auto.
 qed.
 
-(* teorema di prova che non compila per via del let *)
-theorem le_gen_S_x_2: \forall m,x. (le (S m) x) \to let k \def (S O) in
-                      (\exists n. x = (S n) \land (le m n) \land k = k).
+theorem le_gen_S_x_2: \forall m,x. (le (S m) x) \to
+                        \exists n. x = (S n) \land (le m n).
 intros.
 lapply le_gen_S_x to H using H0. elim H0. elim H1.
 exists. exact x1. auto.
@@ -102,4 +101,4 @@ theorem le_gen_S_S_2: \forall m,n. (le (S m) (S n)) \to (le m n).
 intros.
 lapply le_gen_S_x_2 to H using H0. elim H0. elim H1. 
 lapply eq_gen_S_S to H2 using H4. rewrite left H4. assumption.
-qed.
\ No newline at end of file
+qed.