reduce with path

[helm.git] / helm / matita / tests / match.ma

diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma
index 732e96fa01c781b2b70e09e9c579e8ef01f5db0c..21bad46a9f8ab8d2c0e5d2c236860c9805c3eaec 100644 (file)
--- a/helm/matita/tests/match.ma
+++ b/helm/matita/tests/match.ma
@@ -290,3 +290,16 @@ intros 2.simplify.elim (leb n1 m1).
 simplify.apply le_n_S.apply H.
 simplify.intros.apply H.apply le_S_n.assumption.
 qed.
+
+theorem prova :
+let three \def (S (S (S O))) in
+let nine \def (times three three) in
+let eightyone \def (times nine nine) in 
+let square \def (times eightyone eightyone) in
+(eq nat square O).
+intro.
+intro.
+intro.intro.
+normalize goal at (? ? % ?).
+
+