X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fex0%2Fprops.ma;h=148879216ca30fefbabaee3675b8da399f34e3ee;hb=89519c7b52e06304a94019dd528925300380cdc0;hp=56620b18f1f0a928e4ee1a3b844dc19a07f21852;hpb=e92710b1d9774a6491122668c8463b8658114610;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma
index 56620b18f..148879216 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma
@@ -46,19 +46,12 @@ nat).(eq A (ASort O n0) (ASort O (S (plus k0 n))))) (refl_equal A (ASort O (S
 nat).(\lambda (_: ((\forall (n0: nat).((le n (S k0)) \to (eq A (asucc gz 
 (aplus gz (ASort n n0) k0)) (ASort O (plus (match n with [O \Rightarrow (S 
 k0) | (S l) \Rightarrow (minus k0 l)]) n0))))))).(\lambda (n0: nat).(\lambda 
-(H0: (le (S n) (S k0))).(ex2_ind nat (\lambda (n1: nat).(eq nat (S k0) (S 
-n1))) (\lambda (n1: nat).(le n n1)) (eq A (asucc gz (aplus gz (ASort (S n) 
-n0) k0)) (ASort O (plus (minus k0 n) n0))) (\lambda (x: nat).(\lambda (H1: 
-(eq nat (S k0) (S x))).(\lambda (H2: (le n x)).(let H3 \def (f_equal nat nat 
-(\lambda (e: nat).(match e in nat return (\lambda (_: nat).nat) with [O 
-\Rightarrow k0 | (S n1) \Rightarrow n1])) (S k0) (S x) H1) in (let H4 \def 
-(eq_ind_r nat x (\lambda (n1: nat).(le n n1)) H2 k0 H3) in (eq_ind A (aplus 
-gz (ASort n n0) k0) (\lambda (a: A).(eq A (asucc gz (aplus gz (ASort (S n) 
-n0) k0)) a)) (eq_ind A (aplus gz (asucc gz (ASort (S n) n0)) k0) (\lambda (a: 
+(H0: (le (S n) (S k0))).(let H_y \def (le_S_n n k0 H0) in (eq_ind A (aplus gz 
+(ASort n n0) k0) (\lambda (a: A).(eq A (asucc gz (aplus gz (ASort (S n) n0) 
+k0)) a)) (eq_ind A (aplus gz (asucc gz (ASort (S n) n0)) k0) (\lambda (a: 
 A).(eq A a (aplus gz (ASort n n0) k0))) (refl_equal A (aplus gz (ASort n n0) 
 k0)) (asucc gz (aplus gz (ASort (S n) n0) k0)) (aplus_asucc gz k0 (ASort (S 
-n) n0))) (ASort O (plus (minus k0 n) n0)) (IH n n0 H4))))))) (le_gen_S n (S 
-k0) H0)))))) h)))) k).
+n) n0))) (ASort O (plus (minus k0 n) n0)) (IH n n0 H_y))))))) h)))) k).
 
 theorem aplus_gz_ge:
  \forall (n: nat).(\forall (k: nat).(\forall (h: nat).((le k h) \to (eq A 
@@ -80,19 +73,12 @@ x)).(let H2 \def (eq_ind nat O (\lambda (ee: nat).(match ee in nat return
 I (S x) H0) in (False_ind (eq A (asucc gz (aplus gz (ASort O n) k0)) (ASort O 
 n)) H2))))) (le_gen_S k0 O H))) (\lambda (n0: nat).(\lambda (_: (((le (S k0) 
 n0) \to (eq A (asucc gz (aplus gz (ASort n0 n) k0)) (ASort (minus n0 (S k0)) 
-n))))).(\lambda (H0: (le (S k0) (S n0))).(ex2_ind nat (\lambda (n1: nat).(eq 
-nat (S n0) (S n1))) (\lambda (n1: nat).(le k0 n1)) (eq A (asucc gz (aplus gz 
-(ASort (S n0) n) k0)) (ASort (minus n0 k0) n)) (\lambda (x: nat).(\lambda 
-(H1: (eq nat (S n0) (S x))).(\lambda (H2: (le k0 x)).(let H3 \def (f_equal 
-nat nat (\lambda (e: nat).(match e in nat return (\lambda (_: nat).nat) with 
-[O \Rightarrow n0 | (S n1) \Rightarrow n1])) (S n0) (S x) H1) in (let H4 \def 
-(eq_ind_r nat x (\lambda (n1: nat).(le k0 n1)) H2 n0 H3) in (eq_ind A (aplus 
-gz (ASort n0 n) k0) (\lambda (a: A).(eq A (asucc gz (aplus gz (ASort (S n0) 
-n) k0)) a)) (eq_ind A (aplus gz (asucc gz (ASort (S n0) n)) k0) (\lambda (a: 
-A).(eq A a (aplus gz (ASort n0 n) k0))) (refl_equal A (aplus gz (ASort n0 n) 
-k0)) (asucc gz (aplus gz (ASort (S n0) n) k0)) (aplus_asucc gz k0 (ASort (S 
-n0) n))) (ASort (minus n0 k0) n) (IH n0 H4))))))) (le_gen_S k0 (S n0) H0))))) 
-h)))) k)).
+n))))).(\lambda (H0: (le (S k0) (S n0))).(let H_y \def (le_S_n k0 n0 H0) in 
+(eq_ind A (aplus gz (ASort n0 n) k0) (\lambda (a: A).(eq A (asucc gz (aplus 
+gz (ASort (S n0) n) k0)) a)) (eq_ind A (aplus gz (asucc gz (ASort (S n0) n)) 
+k0) (\lambda (a: A).(eq A a (aplus gz (ASort n0 n) k0))) (refl_equal A (aplus 
+gz (ASort n0 n) k0)) (asucc gz (aplus gz (ASort (S n0) n) k0)) (aplus_asucc 
+gz k0 (ASort (S n0) n))) (ASort (minus n0 k0) n) (IH n0 H_y)))))) h)))) k)).
 
 theorem next_plus_gz:
  \forall (n: nat).(\forall (h: nat).(eq nat (next_plus gz n h) (plus h n)))