update in basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_1/T/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/T/fwd.ma
index 159a244681ea9dd21bc45890fee45fcf3910a2f8..5e1833cc17b0d50efe1271d388552cd15f3d86aa 100644 (file)
--- 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)