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

diff --git a/matita/matita/contribs/lambdadelta/basic_1/arity/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/arity/fwd.ma
index 58775a829..78211905a 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/arity/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/arity/fwd.ma
@@ -20,7 +20,7 @@ include "basic_1/leq/asucc.ma".
 
 include "basic_1/getl/drop.ma".
 
-implied let rec arity_ind (g: G) (P: (C \to (T \to (A \to Prop)))) (f: 
+implied rec lemma arity_ind (g: G) (P: (C \to (T \to (A \to Prop)))) (f: 
 (\forall (c: C).(\forall (n: nat).(P c (TSort n) (ASort O n))))) (f0: 
 (\forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c 
 (CHead d (Bind Abbr) u)) \to (\forall (a: A).((arity g d u a) \to ((P d u a)