X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Flegacy_1%2Fcoq%2Ffwd.ma;h=c11c7d732e37831a9eb82484e2bfadf0fa67a38e;hb=ab2f735d97d2b9c965f13527d5f6f61048d29b22;hp=8f5ee7307488b980a1b3a4b4fd6ba3efbff83d9a;hpb=c3904c007394068ed823575e3be3d73a9ad92cce;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma b/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma
index 8f5ee7307..c11c7d732 100644
--- a/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma
@@ -81,12 +81,12 @@ implied lemma eq_ind:
  \lambda (A: Type[0]).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(eq_rect A 
 x P))).
 
-implied let rec le_ind (n: nat) (P: (nat \to Prop)) (f: P n) (f0: (\forall 
+implied rec lemma le_ind (n: nat) (P: (nat \to Prop)) (f: P n) (f0: (\forall 
 (m: nat).((le n m) \to ((P m) \to (P (S m)))))) (n0: nat) (l: le n n0) on l: 
 P n0 \def match l with [le_n \Rightarrow f | (le_S m l0) \Rightarrow (f0 m l0 
 ((le_ind n P f f0) m l0))].
 
-implied let rec Acc_ind (A: Type[0]) (R: (A \to (A \to Prop))) (P: (A \to 
+implied rec lemma Acc_ind (A: Type[0]) (R: (A \to (A \to Prop))) (P: (A \to 
 Prop)) (f: (\forall (x: A).(((\forall (y: A).((R y x) \to (Acc A R y)))) \to 
 (((\forall (y: A).((R y x) \to (P y)))) \to (P x))))) (a: A) (a0: Acc A R a) 
 on a0: P a \def match a0 with [(Acc_intro x a1) \Rightarrow (f x a1 (\lambda