components C r flt app lift

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / tlt / props.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/tlt/props.ma b/matita/matita/contribs/lambdadelta/basic_1/tlt/props.ma
index 584fa7daf1c6d09a3798200afc5f2dfaf37ad424..37cd527fb34e51e8eb765faab54ae9aa3239487d 100644 (file)
--- 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))))).
-