X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftests%2Flambda02.cic.test;fp=helm%2FgTopLevel%2Ftests%2Flambda02.cic.test;h=fde5288f91a4e5e35ad0eb899ee1809d8e8e5232;hb=d8a1a68b8b7e53ba43fcad55e928a99ef5e08b8e;hp=ee8c6b118e11f287ec0e91ea28095faa0b837be6;hpb=feb3c287997f7d35747c12e0db62e6194f5587a3;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))