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

diff --git a/matita/matita/contribs/lambdadelta/basic_1/subst0/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/subst0/fwd.ma
index 5af139ab0..930835ccb 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/subst0/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/subst0/fwd.ma
@@ -18,7 +18,7 @@ include "basic_1/subst0/defs.ma".
 
 include "basic_1/lift/fwd.ma".
 
-implied let rec subst0_ind (P: (nat \to (T \to (T \to (T \to Prop))))) (f: 
+implied rec lemma subst0_ind (P: (nat \to (T \to (T \to (T \to Prop))))) (f: 
 (\forall (v: T).(\forall (i: nat).(P i v (TLRef i) (lift (S i) O v))))) (f0: 
 (\forall (v: T).(\forall (u2: T).(\forall (u1: T).(\forall (i: nat).((subst0 
 i v u1 u2) \to ((P i v u1 u2) \to (\forall (t: T).(\forall (k: K).(P i v