X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fs%2Ffwd.ma;h=deac2dbd3e4604f4cc439391ae3655f2321aee13;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=48a34e79b3a34c5469f80330780bbe21c5695eae;hpb=639e798161afea770f41d78673c0fe3be4125beb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/s/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/s/fwd.ma
index 48a34e79b..deac2dbd3 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/s/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/s/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/s/defs.ma".
 
-theorem s_inj:
+lemma s_inj:
  \forall (k: K).(\forall (i: nat).(\forall (j: nat).((eq nat (s k i) (s k j)) 
 \to (eq nat i j))))
 \def
@@ -26,7 +26,7 @@ B).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (eq nat (s (Bind b) i) (s
 (Bind b) j))).(eq_add_S i j H))))) (\lambda (f: F).(\lambda (i: nat).(\lambda 
 (j: nat).(\lambda (H: (eq nat (s (Flat f) i) (s (Flat f) j))).H)))) k).
 
-theorem s_le_gen:
+lemma s_le_gen:
  \forall (k: K).(\forall (i: nat).(\forall (j: nat).((le (s k i) (s k j)) \to 
 (le i j))))
 \def
@@ -36,7 +36,7 @@ nat).(\lambda (j: nat).(\lambda (H: (le (s (Bind b) i) (s (Bind b)
 j))).(le_S_n i j H))))) (\lambda (f: F).(\lambda (i: nat).(\lambda (j: 
 nat).(\lambda (H: (le (s (Flat f) i) (s (Flat f) j))).H)))) k).
 
-theorem s_lt_gen:
+lemma s_lt_gen:
  \forall (k: K).(\forall (i: nat).(\forall (j: nat).((lt (s k i) (s k j)) \to 
 (lt i j))))
 \def