X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2FT%2Fprops.ma;h=7b62a5a15ed03f87a33fd56e0968900bddbc60b8;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=445f6fc52189b923f185d241d9456d63abb95add;hpb=639e798161afea770f41d78673c0fe3be4125beb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/T/props.ma b/matita/matita/contribs/lambdadelta/basic_1/T/props.ma
index 445f6fc52..7b62a5a15 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/T/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/T/props.ma
@@ -16,35 +16,35 @@
 
 include "basic_1/T/fwd.ma".
 
-theorem not_abbr_abst:
+lemma not_abbr_abst:
  not (eq B Abbr Abst)
 \def
  \lambda (H: (eq B Abbr Abst)).(let H0 \def (eq_ind B Abbr (\lambda (ee: 
 B).(match ee with [Abbr \Rightarrow True | Abst \Rightarrow False | Void 
 \Rightarrow False])) I Abst H) in (False_ind False H0)).
 
-theorem not_void_abst:
+lemma not_void_abst:
  not (eq B Void Abst)
 \def
  \lambda (H: (eq B Void Abst)).(let H0 \def (eq_ind B Void (\lambda (ee: 
 B).(match ee with [Abbr \Rightarrow False | Abst \Rightarrow False | Void 
 \Rightarrow True])) I Abst H) in (False_ind False H0)).
 
-theorem not_abbr_void:
+lemma not_abbr_void:
  not (eq B Abbr Void)
 \def
  \lambda (H: (eq B Abbr Void)).(let H0 \def (eq_ind B Abbr (\lambda (ee: 
 B).(match ee with [Abbr \Rightarrow True | Abst \Rightarrow False | Void 
 \Rightarrow False])) I Void H) in (False_ind False H0)).
 
-theorem not_abst_void:
+lemma not_abst_void:
  not (eq B Abst Void)
 \def
  \lambda (H: (eq B Abst Void)).(let H0 \def (eq_ind B Abst (\lambda (ee: 
 B).(match ee with [Abbr \Rightarrow False | Abst \Rightarrow True | Void 
 \Rightarrow False])) I Void H) in (False_ind False H0)).
 
-theorem tweight_lt:
+lemma tweight_lt:
  \forall (t: T).(lt O (tweight t))
 \def
  \lambda (t: T).(T_ind (\lambda (t0: T).(lt O (tweight t0))) (\lambda (_: 
@@ -53,7 +53,7 @@ nat).(le_n (S O))) (\lambda (_: nat).(le_n (S O))) (\lambda (_: K).(\lambda
 (tweight t1))).(le_S (S O) (plus (tweight t0) (tweight t1)) (le_plus_trans (S 
 O) (tweight t0) (tweight t1) H))))))) t).
 
-theorem tle_r:
+lemma tle_r:
  \forall (t: T).(tle t t)
 \def
  \lambda (t: T).(T_ind (\lambda (t0: T).(le (tweight t0) (tweight t0)))