update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / clear / fwd.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/clear/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/clear/fwd.ma
index 478e65ccaed95fc456e1e2d82bc2e0f2871a0eaa..1b05b45a89c3d9caa3264c5f5d9868c38ad01396 100644 (file)
--- 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)