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

diff --git a/matita/matita/contribs/lambdadelta/basic_1/sty0/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/sty0/fwd.ma
index 5b80b01a2..0d05ca147 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/sty0/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sty0/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/sty0/defs.ma".
 
-implied let rec sty0_ind (g: G) (P: (C \to (T \to (T \to Prop)))) (f: 
+implied rec lemma sty0_ind (g: G) (P: (C \to (T \to (T \to Prop)))) (f: 
 (\forall (c: C).(\forall (n: nat).(P c (TSort n) (TSort (next g n)))))) (f0: 
 (\forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c 
 (CHead d (Bind Abbr) v)) \to (\forall (w: T).((sty0 g d v w) \to ((P d v w)