From db0d3618d7ef673cf3e4892e7deb54984c811144 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 8 Sep 2005 09:42:30 +0000 Subject: [PATCH] completed test --- helm/matita/tests/unfold.ma | 2 ++ 1 file changed, 2 insertions(+) diff --git a/helm/matita/tests/unfold.ma b/helm/matita/tests/unfold.ma index 4af22f1b9..d63dd50d4 100644 --- a/helm/matita/tests/unfold.ma +++ b/helm/matita/tests/unfold.ma @@ -35,3 +35,5 @@ qed. not in the context of the goal. *) theorem t: let uno \def S O in uno + uno = S uno \to uno=uno. intros. unfold uno in H. + reflexivity. +qed. -- 2.39.2