X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fleq%2Ffwd.ma;h=4fc6915b4bc52ead0811aac3d12058ddcdc1bd8b;hb=ab2f735d97d2b9c965f13527d5f6f61048d29b22;hp=32d8e6f870a9fc897d7cf3c57ac7c5fb8e9a33ee;hpb=c3904c007394068ed823575e3be3d73a9ad92cce;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/leq/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/leq/fwd.ma
index 32d8e6f87..4fc6915b4 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/leq/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/leq/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/leq/defs.ma".
 
-implied let rec leq_ind (g: G) (P: (A \to (A \to Prop))) (f: (\forall (h1: 
+implied rec lemma leq_ind (g: G) (P: (A \to (A \to Prop))) (f: (\forall (h1: 
 nat).(\forall (h2: nat).(\forall (n1: nat).(\forall (n2: nat).(\forall (k: 
 nat).((eq A (aplus g (ASort h1 n1) k) (aplus g (ASort h2 n2) k)) \to (P 
 (ASort h1 n1) (ASort h2 n2))))))))) (f0: (\forall (a1: A).(\forall (a2: