From feac5909f11bc7cf2e2d57f4bb7a5729784be483 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 29 Jun 2005 08:51:48 +0000 Subject: [PATCH] Removed a dummy "let ... in" that was there only to show a bug (now fixed). --- helm/matita/tests/fguidi.ma | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) 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. -- 2.39.2