X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2FT%2Ffwd.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2FT%2Ffwd.ma;h=5e1833cc17b0d50efe1271d388552cd15f3d86aa;hb=ab2f735d97d2b9c965f13527d5f6f61048d29b22;hp=159a244681ea9dd21bc45890fee45fcf3910a2f8;hpb=c3904c007394068ed823575e3be3d73a9ad92cce;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/T/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/T/fwd.ma
index 159a24468..5e1833cc1 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/T/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/T/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/T/defs.ma".
 
-implied let rec T_rect (P: (T \to Type[0])) (f: (\forall (n: nat).(P (TSort 
+implied rec lemma T_rect (P: (T \to Type[0])) (f: (\forall (n: nat).(P (TSort 
 n)))) (f0: (\forall (n: nat).(P (TLRef n)))) (f1: (\forall (k: K).(\forall 
 (t: T).((P t) \to (\forall (t0: T).((P t0) \to (P (THead k t t0)))))))) (t: 
 T) on t: P t \def match t with [(TSort n) \Rightarrow (f n) | (TLRef n)