X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Flegacy_1%2Fcoq%2Ffwd.ma;h=8f5ee7307488b980a1b3a4b4fd6ba3efbff83d9a;hb=8de8cf8adfa6fcda91047eb2c25535893ede046a;hp=518bb5ff064f169a3128a6d89ad55521c865d2c8;hpb=d2caaf419cb6c92cb5ca8615f8eac4e12f3ab728;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 518bb5ff0..8f5ee7307 100644
--- a/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma
@@ -16,17 +16,17 @@
 
 include "legacy_1/coq/defs.ma".
 
-theorem False_rect:
+implied lemma False_rect:
  \forall (P: Type[0]).(False \to P)
 \def
  \lambda (P: Type[0]).(\lambda (f: False).(match f in False with [])).
 
-theorem False_ind:
+implied lemma False_ind:
  \forall (P: Prop).(False \to P)
 \def
  \lambda (P: Prop).(False_rect P).
 
-theorem land_rect:
+implied lemma land_rect:
  \forall (A: Prop).(\forall (B: Prop).(\forall (P: Type[0]).(((A \to (B \to 
 P))) \to ((land A B) \to P))))
 \def
@@ -34,13 +34,13 @@ P))) \to ((land A B) \to P))))
 \to (B \to P)))).(\lambda (a: (land A B)).(match a with [(conj x x0) 
 \Rightarrow (f x x0)]))))).
 
-theorem land_ind:
+implied lemma land_ind:
  \forall (A: Prop).(\forall (B: Prop).(\forall (P: Prop).(((A \to (B \to P))) 
 \to ((land A B) \to P))))
 \def
  \lambda (A: Prop).(\lambda (B: Prop).(\lambda (P: Prop).(land_rect A B P))).
 
-theorem or_ind:
+implied lemma or_ind:
  \forall (A: Prop).(\forall (B: Prop).(\forall (P: Prop).(((A \to P)) \to 
 (((B \to P)) \to ((or A B) \to P)))))
 \def
@@ -48,7 +48,7 @@ theorem or_ind:
 P))).(\lambda (f0: ((B \to P))).(\lambda (o: (or A B)).(match o with 
 [(or_introl x) \Rightarrow (f x) | (or_intror x) \Rightarrow (f0 x)])))))).
 
-theorem ex_ind:
+implied lemma ex_ind:
  \forall (A: Type[0]).(\forall (P: ((A \to Prop))).(\forall (P0: 
 Prop).(((\forall (x: A).((P x) \to P0))) \to ((ex A P) \to P0))))
 \def
@@ -56,7 +56,7 @@ Prop).(((\forall (x: A).((P x) \to P0))) \to ((ex A P) \to P0))))
 Prop).(\lambda (f: ((\forall (x: A).((P x) \to P0)))).(\lambda (e: (ex A 
 P)).(match e with [(ex_intro x x0) \Rightarrow (f x x0)]))))).
 
-theorem ex2_ind:
+implied lemma ex2_ind:
  \forall (A: Type[0]).(\forall (P: ((A \to Prop))).(\forall (Q: ((A \to 
 Prop))).(\forall (P0: Prop).(((\forall (x: A).((P x) \to ((Q x) \to P0)))) 
 \to ((ex2 A P Q) \to P0)))))
@@ -66,7 +66,7 @@ Prop))).(\lambda (P0: Prop).(\lambda (f: ((\forall (x: A).((P x) \to ((Q x)
 \to P0))))).(\lambda (e: (ex2 A P Q)).(match e with [(ex_intro2 x x0 x1) 
 \Rightarrow (f x x0 x1)])))))).
 
-theorem eq_rect:
+implied lemma eq_rect:
  \forall (A: Type[0]).(\forall (x: A).(\forall (P: ((A \to Type[0]))).((P x) 
 \to (\forall (y: A).((eq A x y) \to (P y))))))
 \def
@@ -74,21 +74,21 @@ theorem eq_rect:
 Type[0]))).(\lambda (f: (P x)).(\lambda (y: A).(\lambda (e: (eq A x 
 y)).(match e with [refl_equal \Rightarrow f])))))).
 
-theorem eq_ind:
+implied lemma eq_ind:
  \forall (A: Type[0]).(\forall (x: A).(\forall (P: ((A \to Prop))).((P x) \to 
 (\forall (y: A).((eq A x y) \to (P y))))))
 \def
  \lambda (A: Type[0]).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(eq_rect A 
 x P))).
 
-let rec 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 
+implied let rec 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))].
 
-let rec 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 (y: 
-A).(\lambda (r0: (R y x)).((Acc_ind A R P f) y (a1 y r0)))))].
+implied let rec 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 
+(y: A).(\lambda (r0: (R y x)).((Acc_ind A R P f) y (a1 y r0)))))].