X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2FT%2Fprops.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2FT%2Fprops.ma;h=cce311989ed62153b122f9e4bb934af1ca43e409;hb=14a8276e6d877c2281a1fda452ed3e4c150f5d39;hp=9b7a03f1dd104f7d44ba82b75bcc0ff345a74a78;hpb=9c954a9a843ebb1bf189536df4e14f77132ed1cf;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 9b7a03f1d..cce311989 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/T/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/T/props.ma
@@ -19,48 +19,46 @@ include "basic_1/T/fwd.ma".
 theorem not_abbr_abst:
  not (eq B Abbr Abst)
 \def
- \lambda (H: (eq B Abbr Abst)).(let TMP_1 \def (\lambda (ee: B).(match ee in 
-B with [Abbr \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow 
+ \lambda (H: (eq B Abbr Abst)).(let TMP_1 \def (\lambda (ee: B).(match ee 
+with [Abbr \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow 
 False])) in (let H0 \def (eq_ind B Abbr TMP_1 I Abst H) in (False_ind False 
 H0))).
 
 theorem not_void_abst:
  not (eq B Void Abst)
 \def
- \lambda (H: (eq B Void Abst)).(let TMP_2 \def (\lambda (ee: B).(match ee in 
-B with [Abbr \Rightarrow False | Abst \Rightarrow False | Void \Rightarrow 
-True])) in (let H0 \def (eq_ind B Void TMP_2 I Abst H) in (False_ind False 
+ \lambda (H: (eq B Void Abst)).(let TMP_1 \def (\lambda (ee: B).(match ee 
+with [Abbr \Rightarrow False | Abst \Rightarrow False | Void \Rightarrow 
+True])) in (let H0 \def (eq_ind B Void TMP_1 I Abst H) in (False_ind False 
 H0))).
 
 theorem not_abbr_void:
  not (eq B Abbr Void)
 \def
- \lambda (H: (eq B Abbr Void)).(let TMP_3 \def (\lambda (ee: B).(match ee in 
-B with [Abbr \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow 
-False])) in (let H0 \def (eq_ind B Abbr TMP_3 I Void H) in (False_ind False 
+ \lambda (H: (eq B Abbr Void)).(let TMP_1 \def (\lambda (ee: B).(match ee 
+with [Abbr \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow 
+False])) in (let H0 \def (eq_ind B Abbr TMP_1 I Void H) in (False_ind False 
 H0))).
 
 theorem not_abst_void:
  not (eq B Abst Void)
 \def
- \lambda (H: (eq B Abst Void)).(let TMP_4 \def (\lambda (ee: B).(match ee in 
-B with [Abbr \Rightarrow False | Abst \Rightarrow True | Void \Rightarrow 
-False])) in (let H0 \def (eq_ind B Abst TMP_4 I Void H) in (False_ind False 
+ \lambda (H: (eq B Abst Void)).(let TMP_1 \def (\lambda (ee: B).(match ee 
+with [Abbr \Rightarrow False | Abst \Rightarrow True | Void \Rightarrow 
+False])) in (let H0 \def (eq_ind B Abst TMP_1 I Void H) in (False_ind False 
 H0))).
 
 theorem tweight_lt:
  \forall (t: T).(lt O (tweight t))
 \def
- \lambda (t: T).(let TMP_1848 \def (\lambda (t0: T).(let TMP_1847 \def 
-(tweight t0) in (lt O TMP_1847))) in (let TMP_1846 \def (\lambda (_: 
-nat).(let TMP_1845 \def (S O) in (le_n TMP_1845))) in (let TMP_1844 \def 
-(\lambda (_: nat).(let TMP_1843 \def (S O) in (le_n TMP_1843))) in (let 
-TMP_1842 \def (\lambda (_: K).(\lambda (t0: T).(\lambda (H: (lt O (tweight 
-t0))).(\lambda (t1: T).(\lambda (_: (lt O (tweight t1))).(let TMP_1841 \def 
-(S O) in (let TMP_1839 \def (tweight t0) in (let TMP_1838 \def (tweight t1) 
-in (let TMP_1840 \def (plus TMP_1839 TMP_1838) in (let TMP_1836 \def (S O) in 
-(let TMP_1835 \def (tweight t0) in (let TMP_1834 \def (tweight t1) in (let 
-TMP_1837 \def (le_plus_trans TMP_1836 TMP_1835 TMP_1834 H) in (le_S TMP_1841 
-TMP_1840 TMP_1837)))))))))))))) in (T_ind TMP_1848 TMP_1846 TMP_1844 TMP_1842 
-t))))).
+ \lambda (t: T).(let TMP_2 \def (\lambda (t0: T).(let TMP_1 \def (tweight t0) 
+in (lt O TMP_1))) in (let TMP_4 \def (\lambda (_: nat).(let TMP_3 \def (S O) 
+in (le_n TMP_3))) in (let TMP_6 \def (\lambda (_: nat).(let TMP_5 \def (S O) 
+in (le_n TMP_5))) in (let TMP_15 \def (\lambda (_: K).(\lambda (t0: 
+T).(\lambda (H: (lt O (tweight t0))).(\lambda (t1: T).(\lambda (_: (lt O 
+(tweight t1))).(let TMP_7 \def (S O) in (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 O) in (let TMP_12 \def (tweight t0) in (let TMP_13 \def (tweight t1) 
+in (let TMP_14 \def (le_plus_trans TMP_11 TMP_12 TMP_13 H) in (le_S TMP_7 
+TMP_10 TMP_14)))))))))))))) in (T_ind TMP_2 TMP_4 TMP_6 TMP_15 t))))).