From 41a53763963ddaa2bb4af0e1b922525bb9fad84e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 14 Jun 2005 08:13:59 +0000 Subject: [PATCH] incomplete proof terminated --- helm/matita/tests/fix_betareduction.ma | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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. -- 2.39.2