X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Ftlt%2Fprops.ma;h=37cd527fb34e51e8eb765faab54ae9aa3239487d;hb=6d1bb99e7f355d826c07285ba46b6b13a4abaefc;hp=584fa7daf1c6d09a3798200afc5f2dfaf37ad424;hpb=538c5526a6b3c3af44f92c9cc67d82f28995da96;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/tlt/props.ma b/matita/matita/contribs/lambdadelta/basic_1/tlt/props.ma
index 584fa7daf..37cd527fb 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/tlt/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/tlt/props.ma
@@ -415,16 +415,3 @@ TMP_172 \def (weight_map TMP_171 t) in (let TMP_173 \def (le_plus_r TMP_170
 TMP_172) in (le_n_S TMP_163 TMP_168 TMP_173)))))))))))))))) in (K_ind TMP_6 
 TMP_161 TMP_174 k)))).
 
-theorem tle_r:
- \forall (t: T).(tle t t)
-\def
- \lambda (t: T).(let TMP_3 \def (\lambda (t0: T).(let TMP_1 \def (tweight t0) 
-in (let TMP_2 \def (tweight t0) in (le TMP_1 TMP_2)))) in (let TMP_5 \def 
-(\lambda (_: nat).(let TMP_4 \def (S O) in (le_n TMP_4))) in (let TMP_7 \def 
-(\lambda (_: nat).(let TMP_6 \def (S O) in (le_n TMP_6))) in (let TMP_12 \def 
-(\lambda (_: K).(\lambda (t0: T).(\lambda (_: (le (tweight t0) (tweight 
-t0))).(\lambda (t1: T).(\lambda (_: (le (tweight t1) (tweight t1))).(let 
-TMP_8 \def (tweight t0) in (let TMP_9 \def (tweight t1) in (let TMP_10 \def 
-(plus TMP_8 TMP_9) in (let TMP_11 \def (S TMP_10) in (le_n TMP_11)))))))))) 
-in (T_ind TMP_3 TMP_5 TMP_7 TMP_12 t))))).
-