X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fcsubst0%2Ffwd.ma;h=a267513d139456aba64a928835fb84103467a41b;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=724d7c5a96d8c481e46aded90ece0bd97c4a8b84;hpb=8de8cf8adfa6fcda91047eb2c25535893ede046a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubst0/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/csubst0/fwd.ma
index 724d7c5a9..a267513d1 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/csubst0/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/csubst0/fwd.ma
@@ -18,7 +18,7 @@ include "basic_1/csubst0/defs.ma".
 
 include "basic_1/C/fwd.ma".
 
-implied let rec csubst0_ind (P: (nat \to (T \to (C \to (C \to Prop))))) (f: 
+implied rec lemma csubst0_ind (P: (nat \to (T \to (C \to (C \to Prop))))) (f: 
 (\forall (k: K).(\forall (i: nat).(\forall (v: T).(\forall (u1: T).(\forall 
 (u2: T).((subst0 i v u1 u2) \to (\forall (c: C).(P (s k i) v (CHead c k u1) 
 (CHead c k u2)))))))))) (f0: (\forall (k: K).(\forall (i: nat).(\forall (c1: