fix

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

diff --git a/helm/matita/tests/clearbody.ma b/helm/matita/tests/clearbody.ma
index b38de22dbd0ec3866a7d20f2127dce94f677b3cb..29dd2457dae94317c6561786c206d2bb07743e51 100644 (file)
--- a/helm/matita/tests/clearbody.ma
+++ b/helm/matita/tests/clearbody.ma
@@ -19,7 +19,7 @@ alias symbol "plus" (instance 0) = "natural plus".
 
 
 theorem stupid : 
-  let x \def 0 + 1 in x + 1= x + 1.
+  let x \def 0 + 1 in x + 2 = x + 2.
   intros.
   clearbody x. 
   simplify.