X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2Ftests%2Flambda02.cic.test;h=fde5288f91a4e5e35ad0eb899ee1809d8e8e5232;hb=6f0f31787fb03ea4956227e8fcdbc12abd366931;hp=ee8c6b118e11f287ec0e91ea28095faa0b837be6;hpb=cab83f17a2d7a591c4ff2980b07946b50dbf9d00;p=helm.git

diff --git a/helm/gTopLevel/tests/lambda02.cic.test b/helm/gTopLevel/tests/lambda02.cic.test
index ee8c6b118..fde5288f9 100644
--- a/helm/gTopLevel/tests/lambda02.cic.test
+++ b/helm/gTopLevel/tests/lambda02.cic.test
@@ -2,8 +2,8 @@
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)
-[f:(n:nat)(H:(le O n))(eq nat n n)](f O (le_n O))
+[f:(n:nat)((le O n)->(eq nat n n))](f O (le_n O))
 ### (* TYPE_OF the disambiguated term *)
-(f:(n:nat)(H:(le O n))(eq nat n n))(eq nat O O)
+(f:(n:nat)((le O n)->(eq nat n n)))(eq nat O O)
 ### (* REDUCED disambiguated term     *)
-[f:(n:nat)(H:(le O n))(eq nat n n)](f O (le_n O))
+[f:(n:nat)((le O n)->(eq nat n n))](f O (le_n O))