X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fclear%2Ffwd.ma;h=1b05b45a89c3d9caa3264c5f5d9868c38ad01396;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=478e65ccaed95fc456e1e2d82bc2e0f2871a0eaa;hpb=8de8cf8adfa6fcda91047eb2c25535893ede046a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/clear/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/clear/fwd.ma
index 478e65cca..1b05b45a8 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/clear/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/clear/fwd.ma
@@ -18,7 +18,7 @@ include "basic_1/clear/defs.ma".
 
 include "basic_1/C/fwd.ma".
 
-implied let rec clear_ind (P: (C \to (C \to Prop))) (f: (\forall (b: 
+implied rec lemma clear_ind (P: (C \to (C \to Prop))) (f: (\forall (b: 
 B).(\forall (e: C).(\forall (u: T).(P (CHead e (Bind b) u) (CHead e (Bind b) 
 u)))))) (f0: (\forall (e: C).(\forall (c: C).((clear e c) \to ((P e c) \to 
 (\forall (f0: F).(\forall (u: T).(P (CHead e (Flat f0) u) c)))))))) (c: C)