X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fdrop%2Ffwd.ma;h=ed0d67636ed0506c6bef0cfb5a9347946c689f6c;hb=04e33cc90f1d21b6fe65f22723fa513e91e6f321;hp=bb9c1347ce49122d001cc8ba360cc1de7a8408c1;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma
index bb9c1347c..ed0d67636 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-
+set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop/fwd".
 
 include "drop/defs.ma".
 
@@ -24,60 +24,60 @@ h d (CSort n) x) \to (and3 (eq C x (CSort n)) (eq nat h O) (eq nat d O))))))
 \def
  \lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (x: 
 C).(\lambda (H: (drop h d (CSort n) x)).(insert_eq C (CSort n) (\lambda (c: 
-C).(drop h d c x)) (and3 (eq C x (CSort n)) (eq nat h O) (eq nat d O)) 
-(\lambda (y: C).(\lambda (H0: (drop h d y x)).(drop_ind (\lambda (n0: 
+C).(drop h d c x)) (\lambda (c: C).(and3 (eq C x c) (eq nat h O) (eq nat d 
+O))) (\lambda (y: C).(\lambda (H0: (drop h d y x)).(drop_ind (\lambda (n0: 
 nat).(\lambda (n1: nat).(\lambda (c: C).(\lambda (c0: C).((eq C c (CSort n)) 
-\to (and3 (eq C c0 (CSort n)) (eq nat n0 O) (eq nat n1 O))))))) (\lambda (c: 
+\to (and3 (eq C c0 c) (eq nat n0 O) (eq nat n1 O))))))) (\lambda (c: 
 C).(\lambda (H1: (eq C c (CSort n))).(let H2 \def (f_equal C C (\lambda (e: 
 C).e) c (CSort n) H1) in (eq_ind_r C (CSort n) (\lambda (c0: C).(and3 (eq C 
-c0 (CSort n)) (eq nat O O) (eq nat O O))) (and3_intro (eq C (CSort n) (CSort 
-n)) (eq nat O O) (eq nat O O) (refl_equal C (CSort n)) (refl_equal nat O) 
-(refl_equal nat O)) c H2)))) (\lambda (k: K).(\lambda (h0: nat).(\lambda (c: 
-C).(\lambda (e: C).(\lambda (_: (drop (r k h0) O c e)).(\lambda (_: (((eq C c 
-(CSort n)) \to (and3 (eq C e (CSort n)) (eq nat (r k h0) O) (eq nat O 
-O))))).(\lambda (u: T).(\lambda (H3: (eq C (CHead c k u) (CSort n))).(let H4 
-\def (eq_ind C (CHead c k u) (\lambda (ee: C).(match ee in C return (\lambda 
-(_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow 
-True])) I (CSort n) H3) in (False_ind (and3 (eq C e (CSort n)) (eq nat (S h0) 
-O) (eq nat O O)) H4)))))))))) (\lambda (k: K).(\lambda (h0: nat).(\lambda 
-(d0: nat).(\lambda (c: C).(\lambda (e: C).(\lambda (_: (drop h0 (r k d0) c 
-e)).(\lambda (_: (((eq C c (CSort n)) \to (and3 (eq C e (CSort n)) (eq nat h0 
-O) (eq nat (r k d0) O))))).(\lambda (u: T).(\lambda (H3: (eq C (CHead c k 
-(lift h0 (r k d0) u)) (CSort n))).(let H4 \def (eq_ind C (CHead c k (lift h0 
-(r k d0) u)) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) 
+c0 c0) (eq nat O O) (eq nat O O))) (and3_intro (eq C (CSort n) (CSort n)) (eq 
+nat O O) (eq nat O O) (refl_equal C (CSort n)) (refl_equal nat O) (refl_equal 
+nat O)) c H2)))) (\lambda (k: K).(\lambda (h0: nat).(\lambda (c: C).(\lambda 
+(e: C).(\lambda (_: (drop (r k h0) O c e)).(\lambda (_: (((eq C c (CSort n)) 
+\to (and3 (eq C e c) (eq nat (r k h0) O) (eq nat O O))))).(\lambda (u: 
+T).(\lambda (H3: (eq C (CHead c k u) (CSort n))).(let H4 \def (eq_ind C 
+(CHead c k u) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) 
 with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I 
-(CSort n) H3) in (False_ind (and3 (eq C (CHead e k u) (CSort n)) (eq nat h0 
-O) (eq nat (S d0) O)) H4))))))))))) h d y x H0))) H))))).
+(CSort n) H3) in (False_ind (and3 (eq C e (CHead c k u)) (eq nat (S h0) O) 
+(eq nat O O)) H4)))))))))) (\lambda (k: K).(\lambda (h0: nat).(\lambda (d0: 
+nat).(\lambda (c: C).(\lambda (e: C).(\lambda (_: (drop h0 (r k d0) c 
+e)).(\lambda (_: (((eq C c (CSort n)) \to (and3 (eq C e c) (eq nat h0 O) (eq 
+nat (r k d0) O))))).(\lambda (u: T).(\lambda (H3: (eq C (CHead c k (lift h0 
+(r k d0) u)) (CSort n))).(let H4 \def (eq_ind C (CHead c k (lift h0 (r k d0) 
+u)) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort 
+_) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I (CSort n) H3) in 
+(False_ind (and3 (eq C (CHead e k u) (CHead c k (lift h0 (r k d0) u))) (eq 
+nat h0 O) (eq nat (S d0) O)) H4))))))))))) h d y x H0))) H))))).
 
 theorem drop_gen_refl:
  \forall (x: C).(\forall (e: C).((drop O O x e) \to (eq C x e)))
 \def
  \lambda (x: C).(\lambda (e: C).(\lambda (H: (drop O O x e)).(insert_eq nat O 
-(\lambda (n: nat).(drop n O x e)) (eq C x e) (\lambda (y: nat).(\lambda (H0: 
-(drop y O x e)).(insert_eq nat O (\lambda (n: nat).(drop y n x e)) ((eq nat y 
-O) \to (eq C x e)) (\lambda (y0: nat).(\lambda (H1: (drop y y0 x 
-e)).(drop_ind (\lambda (n: nat).(\lambda (n0: nat).(\lambda (c: C).(\lambda 
-(c0: C).((eq nat n0 O) \to ((eq nat n O) \to (eq C c c0))))))) (\lambda (c: 
-C).(\lambda (_: (eq nat O O)).(\lambda (_: (eq nat O O)).(refl_equal C c)))) 
-(\lambda (k: K).(\lambda (h: nat).(\lambda (c: C).(\lambda (e0: C).(\lambda 
-(_: (drop (r k h) O c e0)).(\lambda (_: (((eq nat O O) \to ((eq nat (r k h) 
-O) \to (eq C c e0))))).(\lambda (u: T).(\lambda (_: (eq nat O O)).(\lambda 
-(H5: (eq nat (S h) O)).(let H6 \def (eq_ind nat (S h) (\lambda (ee: 
-nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow 
-False | (S _) \Rightarrow True])) I O H5) in (False_ind (eq C (CHead c k u) 
-e0) H6))))))))))) (\lambda (k: K).(\lambda (h: nat).(\lambda (d: 
-nat).(\lambda (c: C).(\lambda (e0: C).(\lambda (H2: (drop h (r k d) c 
-e0)).(\lambda (H3: (((eq nat (r k d) O) \to ((eq nat h O) \to (eq C c 
+(\lambda (n: nat).(drop n O x e)) (\lambda (_: nat).(eq C x e)) (\lambda (y: 
+nat).(\lambda (H0: (drop y O x e)).(insert_eq nat O (\lambda (n: nat).(drop y 
+n x e)) (\lambda (n: nat).((eq nat y n) \to (eq C x e))) (\lambda (y0: 
+nat).(\lambda (H1: (drop y y0 x e)).(drop_ind (\lambda (n: nat).(\lambda (n0: 
+nat).(\lambda (c: C).(\lambda (c0: C).((eq nat n0 O) \to ((eq nat n n0) \to 
+(eq C c c0))))))) (\lambda (c: C).(\lambda (_: (eq nat O O)).(\lambda (_: (eq 
+nat O O)).(refl_equal C c)))) (\lambda (k: K).(\lambda (h: nat).(\lambda (c: 
+C).(\lambda (e0: C).(\lambda (_: (drop (r k h) O c e0)).(\lambda (_: (((eq 
+nat O O) \to ((eq nat (r k h) O) \to (eq C c e0))))).(\lambda (u: T).(\lambda 
+(_: (eq nat O O)).(\lambda (H5: (eq nat (S h) O)).(let H6 \def (eq_ind nat (S 
+h) (\lambda (ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O 
+\Rightarrow False | (S _) \Rightarrow True])) I O H5) in (False_ind (eq C 
+(CHead c k u) e0) H6))))))))))) (\lambda (k: K).(\lambda (h: nat).(\lambda 
+(d: nat).(\lambda (c: C).(\lambda (e0: C).(\lambda (H2: (drop h (r k d) c 
+e0)).(\lambda (H3: (((eq nat (r k d) O) \to ((eq nat h (r k d)) \to (eq C c 
 e0))))).(\lambda (u: T).(\lambda (H4: (eq nat (S d) O)).(\lambda (H5: (eq nat 
-h O)).(let H6 \def (f_equal nat nat (\lambda (e1: nat).e1) h O H5) in (let H7 
-\def (eq_ind nat h (\lambda (n: nat).((eq nat (r k d) O) \to ((eq nat n O) 
-\to (eq C c e0)))) H3 O H6) in (let H8 \def (eq_ind nat h (\lambda (n: 
-nat).(drop n (r k d) c e0)) H2 O H6) in (eq_ind_r nat O (\lambda (n: nat).(eq 
-C (CHead c k (lift n (r k d) u)) (CHead e0 k u))) (let H9 \def (eq_ind nat (S 
-d) (\lambda (ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O 
-\Rightarrow False | (S _) \Rightarrow True])) I O H4) in (False_ind (eq C 
-(CHead c k (lift O (r k d) u)) (CHead e0 k u)) H9)) h H6)))))))))))))) y y0 x 
-e H1))) H0))) H))).
+h (S d))).(let H6 \def (f_equal nat nat (\lambda (e1: nat).e1) h (S d) H5) in 
+(let H7 \def (eq_ind nat h (\lambda (n: nat).((eq nat (r k d) O) \to ((eq nat 
+n (r k d)) \to (eq C c e0)))) H3 (S d) H6) in (let H8 \def (eq_ind nat h 
+(\lambda (n: nat).(drop n (r k d) c e0)) H2 (S d) H6) in (eq_ind_r nat (S d) 
+(\lambda (n: nat).(eq C (CHead c k (lift n (r k d) u)) (CHead e0 k u))) (let 
+H9 \def (eq_ind nat (S d) (\lambda (ee: nat).(match ee in nat return (\lambda 
+(_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H4) 
+in (False_ind (eq C (CHead c k (lift (S d) (r k d) u)) (CHead e0 k u)) H9)) h 
+H6)))))))))))))) y y0 x e H1))) H0))) H))).
 
 theorem drop_gen_drop:
  \forall (k: K).(\forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h: 
@@ -85,25 +85,26 @@ nat).((drop (S h) O (CHead c k u) x) \to (drop (r k h) O c x))))))
 \def
  \lambda (k: K).(\lambda (c: C).(\lambda (x: C).(\lambda (u: T).(\lambda (h: 
 nat).(\lambda (H: (drop (S h) O (CHead c k u) x)).(insert_eq C (CHead c k u) 
-(\lambda (c0: C).(drop (S h) O c0 x)) (drop (r k h) O c x) (\lambda (y: 
-C).(\lambda (H0: (drop (S h) O y x)).(insert_eq nat O (\lambda (n: nat).(drop 
-(S h) n y x)) ((eq C y (CHead c k u)) \to (drop (r k h) O c x)) (\lambda (y0: 
-nat).(\lambda (H1: (drop (S h) y0 y x)).(insert_eq nat (S h) (\lambda (n: 
-nat).(drop n y0 y x)) ((eq nat y0 O) \to ((eq C y (CHead c k u)) \to (drop (r 
-k h) O c x))) (\lambda (y1: nat).(\lambda (H2: (drop y1 y0 y x)).(drop_ind 
-(\lambda (n: nat).(\lambda (n0: nat).(\lambda (c0: C).(\lambda (c1: C).((eq 
-nat n (S h)) \to ((eq nat n0 O) \to ((eq C c0 (CHead c k u)) \to (drop (r k 
-h) O c c1)))))))) (\lambda (c0: C).(\lambda (H3: (eq nat O (S h))).(\lambda 
-(_: (eq nat O O)).(\lambda (_: (eq C c0 (CHead c k u))).(let H6 \def (match 
-H3 in eq return (\lambda (n: nat).(\lambda (_: (eq ? ? n)).((eq nat n (S h)) 
-\to (drop (r k h) O c c0)))) with [refl_equal \Rightarrow (\lambda (H6: (eq 
-nat O (S h))).(let H7 \def (eq_ind nat O (\lambda (e: nat).(match e in nat 
-return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow 
-False])) I (S h) H6) in (False_ind (drop (r k h) O c c0) H7)))]) in (H6 
-(refl_equal nat (S h)))))))) (\lambda (k0: K).(\lambda (h0: nat).(\lambda 
-(c0: C).(\lambda (e: C).(\lambda (H3: (drop (r k0 h0) O c0 e)).(\lambda (_: 
-(((eq nat (r k0 h0) (S h)) \to ((eq nat O O) \to ((eq C c0 (CHead c k u)) \to 
-(drop (r k h) O c e)))))).(\lambda (u0: T).(\lambda (H5: (eq nat (S h0) (S 
+(\lambda (c0: C).(drop (S h) O c0 x)) (\lambda (_: C).(drop (r k h) O c x)) 
+(\lambda (y: C).(\lambda (H0: (drop (S h) O y x)).(insert_eq nat O (\lambda 
+(n: nat).(drop (S h) n y x)) (\lambda (n: nat).((eq C y (CHead c k u)) \to 
+(drop (r k h) n c x))) (\lambda (y0: nat).(\lambda (H1: (drop (S h) y0 y 
+x)).(insert_eq nat (S h) (\lambda (n: nat).(drop n y0 y x)) (\lambda (_: 
+nat).((eq nat y0 O) \to ((eq C y (CHead c k u)) \to (drop (r k h) y0 c x)))) 
+(\lambda (y1: nat).(\lambda (H2: (drop y1 y0 y x)).(drop_ind (\lambda (n: 
+nat).(\lambda (n0: nat).(\lambda (c0: C).(\lambda (c1: C).((eq nat n (S h)) 
+\to ((eq nat n0 O) \to ((eq C c0 (CHead c k u)) \to (drop (r k h) n0 c 
+c1)))))))) (\lambda (c0: C).(\lambda (H3: (eq nat O (S h))).(\lambda (_: (eq 
+nat O O)).(\lambda (_: (eq C c0 (CHead c k u))).(let H6 \def (match H3 in eq 
+return (\lambda (n: nat).(\lambda (_: (eq ? ? n)).((eq nat n (S h)) \to (drop 
+(r k h) O c c0)))) with [refl_equal \Rightarrow (\lambda (H6: (eq nat O (S 
+h))).(let H7 \def (eq_ind nat O (\lambda (e: nat).(match e in nat return 
+(\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False])) 
+I (S h) H6) in (False_ind (drop (r k h) O c c0) H7)))]) in (H6 (refl_equal 
+nat (S h)))))))) (\lambda (k0: K).(\lambda (h0: nat).(\lambda (c0: 
+C).(\lambda (e: C).(\lambda (H3: (drop (r k0 h0) O c0 e)).(\lambda (_: (((eq 
+nat (r k0 h0) (S h)) \to ((eq nat O O) \to ((eq C c0 (CHead c k u)) \to (drop 
+(r k h) O c e)))))).(\lambda (u0: T).(\lambda (H5: (eq nat (S h0) (S 
 h))).(\lambda (_: (eq nat O O)).(\lambda (H7: (eq C (CHead c0 k0 u0) (CHead c 
 k u))).(let H8 \def (match H5 in eq return (\lambda (n: nat).(\lambda (_: (eq 
 ? ? n)).((eq nat n (S h)) \to (drop (r k h) O c e)))) with [refl_equal 
@@ -132,14 +133,14 @@ in (H10 (refl_equal C (CHead c k u)))) h0 (sym_eq nat h0 h H9))))]) in (H8
 (refl_equal nat (S h)))))))))))))) (\lambda (k0: K).(\lambda (h0: 
 nat).(\lambda (d: nat).(\lambda (c0: C).(\lambda (e: C).(\lambda (_: (drop h0 
 (r k0 d) c0 e)).(\lambda (_: (((eq nat h0 (S h)) \to ((eq nat (r k0 d) O) \to 
-((eq C c0 (CHead c k u)) \to (drop (r k h) O c e)))))).(\lambda (u0: 
+((eq C c0 (CHead c k u)) \to (drop (r k h) (r k0 d) c e)))))).(\lambda (u0: 
 T).(\lambda (_: (eq nat h0 (S h))).(\lambda (H6: (eq nat (S d) O)).(\lambda 
 (_: (eq C (CHead c0 k0 (lift h0 (r k0 d) u0)) (CHead c k u))).(let H8 \def 
 (match H6 in eq return (\lambda (n: nat).(\lambda (_: (eq ? ? n)).((eq nat n 
-O) \to (drop (r k h) O c (CHead e k0 u0))))) with [refl_equal \Rightarrow 
+O) \to (drop (r k h) (S d) c (CHead e k0 u0))))) with [refl_equal \Rightarrow 
 (\lambda (H8: (eq nat (S d) O)).(let H9 \def (eq_ind nat (S d) (\lambda (e0: 
 nat).(match e0 in nat return (\lambda (_: nat).Prop) with [O \Rightarrow 
-False | (S _) \Rightarrow True])) I O H8) in (False_ind (drop (r k h) O c 
+False | (S _) \Rightarrow True])) I O H8) in (False_ind (drop (r k h) (S d) c 
 (CHead e k0 u0)) H9)))]) in (H8 (refl_equal nat O)))))))))))))) y1 y0 y x 
 H2))) H1))) H0))) H)))))).