X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2FT%2Fprops.ma;h=95088bb195446dd2bda92b5b52d9b7bcdb147cec;hb=7f82161596bdfccc1179f5edcc0bfd76d34516b5;hp=a9c293f20f1ebaacbc153a6be38337ae49ef0147;hpb=892560610e438da6ada9adc42fcc3dd94a0438b9;p=helm.git

diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/props.ma
index a9c293f20..95088bb19 100644
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/props.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/props.ma
@@ -67,3 +67,12 @@ v (\lambda (t: T).((eq T (THead k t t1) t1) \to (\forall (P: Prop).P))) H0 t0
 H5) in (let H8 \def (eq_ind K k (\lambda (k: K).((eq T (THead k t0 t1) t1) 
 \to (\forall (P: Prop).P))) H7 k0 H6) in (H8 H4 P)))))) H3)) H2))))))))) t))).
 
+theorem tweight_lt:
+ \forall (t: T).(lt O (tweight t))
+\def
+ \lambda (t: T).(match t in T return (\lambda (t0: T).(lt O (tweight t0))) 
+with [(TSort _) \Rightarrow (le_n (S O)) | (TLRef _) \Rightarrow (le_n (S O)) 
+| (THead _ t0 t1) \Rightarrow (le_S_n (S O) (S (plus (tweight t0) (tweight 
+t1))) (le_n_S (S O) (S (plus (tweight t0) (tweight t1))) (le_n_S O (plus 
+(tweight t0) (tweight t1)) (le_O_n (plus (tweight t0) (tweight t1))))))]).
+