From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 14 Jun 2005 08:13:59 +0000 (+0000)
Subject: incomplete proof terminated
X-Git-Tag: PRE_STORAGE~37
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=41a53763963ddaa2bb4af0e1b922525bb9fad84e;p=helm.git

incomplete proof terminated
---

diff --git a/helm/matita/tests/fix_betareduction.ma b/helm/matita/tests/fix_betareduction.ma
index 32f298d60..5056f9e6e 100644
--- a/helm/matita/tests/fix_betareduction.ma
+++ b/helm/matita/tests/fix_betareduction.ma
@@ -5,4 +5,6 @@ theorem a:
   (\forall p: nat \to Prop.
   \forall n: nat. p n \to p n ) \to (eq nat n n).
 intro.
-apply (H (\lambda n:nat.(eq nat n n))).
\ No newline at end of file
+apply (H (\lambda n:nat.(eq nat n n))).
+reflexivity.
+qed.