components: clen lift1 drop1

diff --git a/matita/matita/contribs/lambdadelta/basic_1/clen/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/clen/defs.ma
index 07539ffadcf601c2d4f54ec78c9e0d9f39b0eef2..a70c3ef675ba6be06dd199d0c4638b85bb3b07a7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/clen/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/clen/defs.ma
@@ -14,13 +14,10 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/C/defs.ma".
+include "basic_1/C/defs.ma".
 
-include "Basic-1/s/defs.ma".
+include "basic_1/s/defs.ma".
 
-definition clen:
- C \to nat
-\def
- let rec clen (c: C) on c: nat \def (match c with [(CSort _) \Rightarrow O | 
-(CHead c0 k _) \Rightarrow (s k (clen c0))]) in clen.
+let rec clen (c: C) on c: nat \def match c with [(CSort _) \Rightarrow O | 
+(CHead c0 k _) \Rightarrow (let TMP_1 \def (clen c0) in (s k TMP_1))].
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/clen/getl.ma b/matita/matita/contribs/lambdadelta/basic_1/clen/getl.ma
index af8a96cf556dfbfe173c76fd4d6e06a3a758d5ad..ac47a2a4486d9d9748bde2ae06001119a5e067f8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/clen/getl.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/clen/getl.ma
@@ -14,36 +14,64 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/clen/defs.ma".
+include "basic_1/clen/defs.ma".
 
-include "Basic-1/getl/props.ma".
+include "basic_1/getl/props.ma".
 
 theorem getl_ctail_clen:
  \forall (b: B).(\forall (t: T).(\forall (c: C).(ex nat (\lambda (n: 
 nat).(getl (clen c) (CTail (Bind b) t c) (CHead (CSort n) (Bind b) t))))))
 \def
- \lambda (b: B).(\lambda (t: T).(\lambda (c: C).(C_ind (\lambda (c0: C).(ex 
-nat (\lambda (n: nat).(getl (clen c0) (CTail (Bind b) t c0) (CHead (CSort n) 
-(Bind b) t))))) (\lambda (n: nat).(ex_intro nat (\lambda (n0: nat).(getl O 
-(CHead (CSort n) (Bind b) t) (CHead (CSort n0) (Bind b) t))) n (getl_refl b 
-(CSort n) t))) (\lambda (c0: C).(\lambda (H: (ex nat (\lambda (n: nat).(getl 
-(clen c0) (CTail (Bind b) t c0) (CHead (CSort n) (Bind b) t))))).(\lambda (k: 
-K).(\lambda (t0: T).(let H0 \def H in (ex_ind nat (\lambda (n: nat).(getl 
-(clen c0) (CTail (Bind b) t c0) (CHead (CSort n) (Bind b) t))) (ex nat 
-(\lambda (n: nat).(getl (s k (clen c0)) (CHead (CTail (Bind b) t c0) k t0) 
-(CHead (CSort n) (Bind b) t)))) (\lambda (x: nat).(\lambda (H1: (getl (clen 
-c0) (CTail (Bind b) t c0) (CHead (CSort x) (Bind b) t))).(K_ind (\lambda (k0: 
-K).(ex nat (\lambda (n: nat).(getl (s k0 (clen c0)) (CHead (CTail (Bind b) t 
-c0) k0 t0) (CHead (CSort n) (Bind b) t))))) (\lambda (b0: B).(ex_intro nat 
-(\lambda (n: nat).(getl (S (clen c0)) (CHead (CTail (Bind b) t c0) (Bind b0) 
-t0) (CHead (CSort n) (Bind b) t))) x (getl_head (Bind b0) (clen c0) (CTail 
-(Bind b) t c0) (CHead (CSort x) (Bind b) t) H1 t0))) (\lambda (f: 
-F).(ex_intro nat (\lambda (n: nat).(getl (clen c0) (CHead (CTail (Bind b) t 
-c0) (Flat f) t0) (CHead (CSort n) (Bind b) t))) x (getl_flat (CTail (Bind b) 
-t c0) (CHead (CSort x) (Bind b) t) (clen c0) H1 f t0))) k))) H0)))))) c))).
-(* COMMENTS
-Initial nodes: 459
-END *)
+ \lambda (b: B).(\lambda (t: T).(\lambda (c: C).(let TMP_8 \def (\lambda (c0: 
+C).(let TMP_7 \def (\lambda (n: nat).(let TMP_1 \def (clen c0) in (let TMP_2 
+\def (Bind b) in (let TMP_3 \def (CTail TMP_2 t c0) in (let TMP_4 \def (CSort 
+n) in (let TMP_5 \def (Bind b) in (let TMP_6 \def (CHead TMP_4 TMP_5 t) in 
+(getl TMP_1 TMP_3 TMP_6)))))))) in (ex nat TMP_7))) in (let TMP_18 \def 
+(\lambda (n: nat).(let TMP_15 \def (\lambda (n0: nat).(let TMP_9 \def (CSort 
+n) in (let TMP_10 \def (Bind b) in (let TMP_11 \def (CHead TMP_9 TMP_10 t) in 
+(let TMP_12 \def (CSort n0) in (let TMP_13 \def (Bind b) in (let TMP_14 \def 
+(CHead TMP_12 TMP_13 t) in (getl O TMP_11 TMP_14)))))))) in (let TMP_16 \def 
+(CSort n) in (let TMP_17 \def (getl_refl b TMP_16 t) in (ex_intro nat TMP_15 
+n TMP_17))))) in (let TMP_83 \def (\lambda (c0: C).(\lambda (H: (ex nat 
+(\lambda (n: nat).(getl (clen c0) (CTail (Bind b) t c0) (CHead (CSort n) 
+(Bind b) t))))).(\lambda (k: K).(\lambda (t0: T).(let H0 \def H in (let 
+TMP_25 \def (\lambda (n: nat).(let TMP_19 \def (clen c0) in (let TMP_20 \def 
+(Bind b) in (let TMP_21 \def (CTail TMP_20 t c0) in (let TMP_22 \def (CSort 
+n) in (let TMP_23 \def (Bind b) in (let TMP_24 \def (CHead TMP_22 TMP_23 t) 
+in (getl TMP_19 TMP_21 TMP_24)))))))) in (let TMP_34 \def (\lambda (n: 
+nat).(let TMP_26 \def (clen c0) in (let TMP_27 \def (s k TMP_26) in (let 
+TMP_28 \def (Bind b) in (let TMP_29 \def (CTail TMP_28 t c0) in (let TMP_30 
+\def (CHead TMP_29 k t0) in (let TMP_31 \def (CSort n) in (let TMP_32 \def 
+(Bind b) in (let TMP_33 \def (CHead TMP_31 TMP_32 t) in (getl TMP_27 TMP_30 
+TMP_33)))))))))) in (let TMP_35 \def (ex nat TMP_34) in (let TMP_82 \def 
+(\lambda (x: nat).(\lambda (H1: (getl (clen c0) (CTail (Bind b) t c0) (CHead 
+(CSort x) (Bind b) t))).(let TMP_45 \def (\lambda (k0: K).(let TMP_44 \def 
+(\lambda (n: nat).(let TMP_36 \def (clen c0) in (let TMP_37 \def (s k0 
+TMP_36) in (let TMP_38 \def (Bind b) in (let TMP_39 \def (CTail TMP_38 t c0) 
+in (let TMP_40 \def (CHead TMP_39 k0 t0) in (let TMP_41 \def (CSort n) in 
+(let TMP_42 \def (Bind b) in (let TMP_43 \def (CHead TMP_41 TMP_42 t) in 
+(getl TMP_37 TMP_40 TMP_43)))))))))) in (ex nat TMP_44))) in (let TMP_64 \def 
+(\lambda (b0: B).(let TMP_55 \def (\lambda (n: nat).(let TMP_46 \def (clen 
+c0) in (let TMP_47 \def (S TMP_46) in (let TMP_48 \def (Bind b) in (let 
+TMP_49 \def (CTail TMP_48 t c0) in (let TMP_50 \def (Bind b0) in (let TMP_51 
+\def (CHead TMP_49 TMP_50 t0) in (let TMP_52 \def (CSort n) in (let TMP_53 
+\def (Bind b) in (let TMP_54 \def (CHead TMP_52 TMP_53 t) in (getl TMP_47 
+TMP_51 TMP_54))))))))))) in (let TMP_56 \def (Bind b0) in (let TMP_57 \def 
+(clen c0) in (let TMP_58 \def (Bind b) in (let TMP_59 \def (CTail TMP_58 t 
+c0) in (let TMP_60 \def (CSort x) in (let TMP_61 \def (Bind b) in (let TMP_62 
+\def (CHead TMP_60 TMP_61 t) in (let TMP_63 \def (getl_head TMP_56 TMP_57 
+TMP_59 TMP_62 H1 t0) in (ex_intro nat TMP_55 x TMP_63))))))))))) in (let 
+TMP_81 \def (\lambda (f: F).(let TMP_73 \def (\lambda (n: nat).(let TMP_65 
+\def (clen c0) in (let TMP_66 \def (Bind b) in (let TMP_67 \def (CTail TMP_66 
+t c0) in (let TMP_68 \def (Flat f) in (let TMP_69 \def (CHead TMP_67 TMP_68 
+t0) in (let TMP_70 \def (CSort n) in (let TMP_71 \def (Bind b) in (let TMP_72 
+\def (CHead TMP_70 TMP_71 t) in (getl TMP_65 TMP_69 TMP_72)))))))))) in (let 
+TMP_74 \def (Bind b) in (let TMP_75 \def (CTail TMP_74 t c0) in (let TMP_76 
+\def (CSort x) in (let TMP_77 \def (Bind b) in (let TMP_78 \def (CHead TMP_76 
+TMP_77 t) in (let TMP_79 \def (clen c0) in (let TMP_80 \def (getl_flat TMP_75 
+TMP_78 TMP_79 H1 f t0) in (ex_intro nat TMP_73 x TMP_80)))))))))) in (K_ind 
+TMP_45 TMP_64 TMP_81 k)))))) in (ex_ind nat TMP_25 TMP_35 TMP_82 H0)))))))))) 
+in (C_ind TMP_8 TMP_18 TMP_83 c)))))).
 
 theorem getl_gen_tail:
  \forall (k: K).(\forall (b: B).(\forall (u1: T).(\forall (u2: T).(\forall 
@@ -54,308 +82,737 @@ nat).(eq nat i (clen c1))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
 nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))))))))))
 \def
  \lambda (k: K).(\lambda (b: B).(\lambda (u1: T).(\lambda (u2: T).(\lambda 
-(c2: C).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (i: nat).((getl i 
-(CTail k u1 c) (CHead c2 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C 
-c2 (CTail k u1 e))) (\lambda (e: C).(getl i c (CHead e (Bind b) u2)))) (ex4 
-nat (\lambda (_: nat).(eq nat i (clen c))) (\lambda (_: nat).(eq K k (Bind 
-b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort 
-n)))))))) (\lambda (n: nat).(\lambda (i: nat).(nat_ind (\lambda (n0: 
-nat).((getl n0 (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)) \to (or (ex2 C 
-(\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl n0 (CSort n) 
-(CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat n0 (clen (CSort 
-n)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) 
-(\lambda (n1: nat).(eq C c2 (CSort n1))))))) (\lambda (H: (getl O (CHead 
-(CSort n) k u1) (CHead c2 (Bind b) u2))).(K_ind (\lambda (k0: K).((clear 
-(CHead (CSort n) k0 u1) (CHead c2 (Bind b) u2)) \to (or (ex2 C (\lambda (e: 
-C).(eq C c2 (CTail k0 u1 e))) (\lambda (e: C).(getl O (CSort n) (CHead e 
-(Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O O)) (\lambda (_: 
-nat).(eq K k0 (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: 
-nat).(eq C c2 (CSort n0))))))) (\lambda (b0: B).(\lambda (H0: (clear (CHead 
-(CSort n) (Bind b0) u1) (CHead c2 (Bind b) u2))).(let H1 \def (f_equal C C 
-(\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) 
-\Rightarrow c2 | (CHead c _ _) \Rightarrow c])) (CHead c2 (Bind b) u2) (CHead 
-(CSort n) (Bind b0) u1) (clear_gen_bind b0 (CSort n) (CHead c2 (Bind b) u2) 
-u1 H0)) in ((let H2 \def (f_equal C B (\lambda (e: C).(match e in C return 
-(\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k0 _) \Rightarrow 
-(match k0 in K return (\lambda (_: K).B) with [(Bind b1) \Rightarrow b1 | 
-(Flat _) \Rightarrow b])])) (CHead c2 (Bind b) u2) (CHead (CSort n) (Bind b0) 
-u1) (clear_gen_bind b0 (CSort n) (CHead c2 (Bind b) u2) u1 H0)) in ((let H3 
-\def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) 
-with [(CSort _) \Rightarrow u2 | (CHead _ _ t) \Rightarrow t])) (CHead c2 
-(Bind b) u2) (CHead (CSort n) (Bind b0) u1) (clear_gen_bind b0 (CSort n) 
-(CHead c2 (Bind b) u2) u1 H0)) in (\lambda (H4: (eq B b b0)).(\lambda (H5: 
-(eq C c2 (CSort n))).(eq_ind_r C (CSort n) (\lambda (c: C).(or (ex2 C 
-(\lambda (e: C).(eq C c (CTail (Bind b0) u1 e))) (\lambda (e: C).(getl O 
-(CSort n) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O O)) 
-(\lambda (_: nat).(eq K (Bind b0) (Bind b))) (\lambda (_: nat).(eq T u1 u2)) 
-(\lambda (n0: nat).(eq C c (CSort n0)))))) (eq_ind_r T u1 (\lambda (t: T).(or 
-(ex2 C (\lambda (e: C).(eq C (CSort n) (CTail (Bind b0) u1 e))) (\lambda (e: 
-C).(getl O (CSort n) (CHead e (Bind b) t)))) (ex4 nat (\lambda (_: nat).(eq 
-nat O O)) (\lambda (_: nat).(eq K (Bind b0) (Bind b))) (\lambda (_: nat).(eq 
-T u1 t)) (\lambda (n0: nat).(eq C (CSort n) (CSort n0)))))) (eq_ind_r B b0 
-(\lambda (b1: B).(or (ex2 C (\lambda (e: C).(eq C (CSort n) (CTail (Bind b0) 
-u1 e))) (\lambda (e: C).(getl O (CSort n) (CHead e (Bind b1) u1)))) (ex4 nat 
-(\lambda (_: nat).(eq nat O O)) (\lambda (_: nat).(eq K (Bind b0) (Bind b1))) 
-(\lambda (_: nat).(eq T u1 u1)) (\lambda (n0: nat).(eq C (CSort n) (CSort 
-n0)))))) (or_intror (ex2 C (\lambda (e: C).(eq C (CSort n) (CTail (Bind b0) 
-u1 e))) (\lambda (e: C).(getl O (CSort n) (CHead e (Bind b0) u1)))) (ex4 nat 
-(\lambda (_: nat).(eq nat O O)) (\lambda (_: nat).(eq K (Bind b0) (Bind b0))) 
-(\lambda (_: nat).(eq T u1 u1)) (\lambda (n0: nat).(eq C (CSort n) (CSort 
-n0)))) (ex4_intro nat (\lambda (_: nat).(eq nat O O)) (\lambda (_: nat).(eq K 
-(Bind b0) (Bind b0))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n0: nat).(eq 
-C (CSort n) (CSort n0))) n (refl_equal nat O) (refl_equal K (Bind b0)) 
-(refl_equal T u1) (refl_equal C (CSort n)))) b H4) u2 H3) c2 H5)))) H2)) 
-H1)))) (\lambda (f: F).(\lambda (H0: (clear (CHead (CSort n) (Flat f) u1) 
-(CHead c2 (Bind b) u2))).(clear_gen_sort (CHead c2 (Bind b) u2) n 
-(clear_gen_flat f (CSort n) (CHead c2 (Bind b) u2) u1 H0) (or (ex2 C (\lambda 
-(e: C).(eq C c2 (CTail (Flat f) u1 e))) (\lambda (e: C).(getl O (CSort n) 
-(CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O O)) (\lambda 
-(_: nat).(eq K (Flat f) (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda 
-(n0: nat).(eq C c2 (CSort n0)))))))) k (getl_gen_O (CHead (CSort n) k u1) 
-(CHead c2 (Bind b) u2) H))) (\lambda (n0: nat).(\lambda (_: (((getl n0 (CHead 
-(CSort n) k u1) (CHead c2 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C 
-c2 (CTail k u1 e))) (\lambda (e: C).(getl n0 (CSort n) (CHead e (Bind b) 
-u2)))) (ex4 nat (\lambda (_: nat).(eq nat n0 O)) (\lambda (_: nat).(eq K k 
-(Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n1: nat).(eq C c2 (CSort 
-n1)))))))).(\lambda (H0: (getl (S n0) (CHead (CSort n) k u1) (CHead c2 (Bind 
-b) u2))).(getl_gen_sort n (r k n0) (CHead c2 (Bind b) u2) (getl_gen_S k 
-(CSort n) (CHead c2 (Bind b) u2) u1 n0 H0) (or (ex2 C (\lambda (e: C).(eq C 
-c2 (CTail k u1 e))) (\lambda (e: C).(getl (S n0) (CSort n) (CHead e (Bind b) 
-u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S n0) O)) (\lambda (_: nat).(eq K 
-k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n1: nat).(eq C c2 
-(CSort n1))))))))) i))) (\lambda (c: C).(\lambda (H: ((\forall (i: 
-nat).((getl i (CTail k u1 c) (CHead c2 (Bind b) u2)) \to (or (ex2 C (\lambda 
-(e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl i c (CHead e (Bind b) 
-u2)))) (ex4 nat (\lambda (_: nat).(eq nat i (clen c))) (\lambda (_: nat).(eq 
-K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 
-(CSort n))))))))).(\lambda (k0: K).(\lambda (t: T).(\lambda (i: nat).(nat_ind 
-(\lambda (n: nat).((getl n (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) 
-u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: 
-C).(getl n (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: 
-nat).(eq nat n (clen (CHead c k0 t)))) (\lambda (_: nat).(eq K k (Bind b))) 
-(\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))))) 
-(\lambda (H0: (getl O (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) 
-u2))).(K_ind (\lambda (k1: K).((clear (CHead (CTail k u1 c) k1 t) (CHead c2 
+(c2: C).(\lambda (c1: C).(let TMP_15 \def (\lambda (c: C).(\forall (i: 
+nat).((getl i (CTail k u1 c) (CHead c2 (Bind b) u2)) \to (let TMP_2 \def 
+(\lambda (e: C).(let TMP_1 \def (CTail k u1 e) in (eq C c2 TMP_1))) in (let 
+TMP_5 \def (\lambda (e: C).(let TMP_3 \def (Bind b) in (let TMP_4 \def (CHead 
+e TMP_3 u2) in (getl i c TMP_4)))) in (let TMP_6 \def (ex2 C TMP_2 TMP_5) in 
+(let TMP_8 \def (\lambda (_: nat).(let TMP_7 \def (clen c) in (eq nat i 
+TMP_7))) in (let TMP_10 \def (\lambda (_: nat).(let TMP_9 \def (Bind b) in 
+(eq K k TMP_9))) in (let TMP_11 \def (\lambda (_: nat).(eq T u1 u2)) in (let 
+TMP_13 \def (\lambda (n: nat).(let TMP_12 \def (CSort n) in (eq C c2 
+TMP_12))) in (let TMP_14 \def (ex4 nat TMP_8 TMP_10 TMP_11 TMP_13) in (or 
+TMP_6 TMP_14)))))))))))) in (let TMP_228 \def (\lambda (n: nat).(\lambda (i: 
+nat).(let TMP_32 \def (\lambda (n0: nat).((getl n0 (CTail k u1 (CSort n)) 
+(CHead c2 (Bind b) u2)) \to (let TMP_17 \def (\lambda (e: C).(let TMP_16 \def 
+(CTail k u1 e) in (eq C c2 TMP_16))) in (let TMP_21 \def (\lambda (e: C).(let 
+TMP_18 \def (CSort n) in (let TMP_19 \def (Bind b) in (let TMP_20 \def (CHead 
+e TMP_19 u2) in (getl n0 TMP_18 TMP_20))))) in (let TMP_22 \def (ex2 C TMP_17 
+TMP_21) in (let TMP_25 \def (\lambda (_: nat).(let TMP_23 \def (CSort n) in 
+(let TMP_24 \def (clen TMP_23) in (eq nat n0 TMP_24)))) in (let TMP_27 \def 
+(\lambda (_: nat).(let TMP_26 \def (Bind b) in (eq K k TMP_26))) in (let 
+TMP_28 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_30 \def (\lambda (n1: 
+nat).(let TMP_29 \def (CSort n1) in (eq C c2 TMP_29))) in (let TMP_31 \def 
+(ex4 nat TMP_25 TMP_27 TMP_28 TMP_30) in (or TMP_22 TMP_31))))))))))) in (let 
+TMP_202 \def (\lambda (H: (getl O (CHead (CSort n) k u1) (CHead c2 (Bind b) 
+u2))).(let TMP_47 \def (\lambda (k0: K).((clear (CHead (CSort n) k0 u1) 
+(CHead c2 (Bind b) u2)) \to (let TMP_34 \def (\lambda (e: C).(let TMP_33 \def 
+(CTail k0 u1 e) in (eq C c2 TMP_33))) in (let TMP_38 \def (\lambda (e: 
+C).(let TMP_35 \def (CSort n) in (let TMP_36 \def (Bind b) in (let TMP_37 
+\def (CHead e TMP_36 u2) in (getl O TMP_35 TMP_37))))) in (let TMP_39 \def 
+(ex2 C TMP_34 TMP_38) in (let TMP_40 \def (\lambda (_: nat).(eq nat O O)) in 
+(let TMP_42 \def (\lambda (_: nat).(let TMP_41 \def (Bind b) in (eq K k0 
+TMP_41))) in (let TMP_43 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_45 
+\def (\lambda (n0: nat).(let TMP_44 \def (CSort n0) in (eq C c2 TMP_44))) in 
+(let TMP_46 \def (ex4 nat TMP_40 TMP_42 TMP_43 TMP_45) in (or TMP_39 
+TMP_46))))))))))) in (let TMP_172 \def (\lambda (b0: B).(\lambda (H0: (clear 
+(CHead (CSort n) (Bind b0) u1) (CHead c2 (Bind b) u2))).(let TMP_48 \def 
+(\lambda (e: C).(match e with [(CSort _) \Rightarrow c2 | (CHead c _ _) 
+\Rightarrow c])) in (let TMP_49 \def (Bind b) in (let TMP_50 \def (CHead c2 
+TMP_49 u2) in (let TMP_51 \def (CSort n) in (let TMP_52 \def (Bind b0) in 
+(let TMP_53 \def (CHead TMP_51 TMP_52 u1) in (let TMP_54 \def (CSort n) in 
+(let TMP_55 \def (Bind b) in (let TMP_56 \def (CHead c2 TMP_55 u2) in (let 
+TMP_57 \def (clear_gen_bind b0 TMP_54 TMP_56 u1 H0) in (let H1 \def (f_equal 
+C C TMP_48 TMP_50 TMP_53 TMP_57) in (let TMP_58 \def (\lambda (e: C).(match e 
+with [(CSort _) \Rightarrow b | (CHead _ k0 _) \Rightarrow (match k0 with 
+[(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow b])])) in (let TMP_59 \def 
+(Bind b) in (let TMP_60 \def (CHead c2 TMP_59 u2) in (let TMP_61 \def (CSort 
+n) in (let TMP_62 \def (Bind b0) in (let TMP_63 \def (CHead TMP_61 TMP_62 u1) 
+in (let TMP_64 \def (CSort n) in (let TMP_65 \def (Bind b) in (let TMP_66 
+\def (CHead c2 TMP_65 u2) in (let TMP_67 \def (clear_gen_bind b0 TMP_64 
+TMP_66 u1 H0) in (let H2 \def (f_equal C B TMP_58 TMP_60 TMP_63 TMP_67) in 
+(let TMP_68 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow u2 | 
+(CHead _ _ t) \Rightarrow t])) in (let TMP_69 \def (Bind b) in (let TMP_70 
+\def (CHead c2 TMP_69 u2) in (let TMP_71 \def (CSort n) in (let TMP_72 \def 
+(Bind b0) in (let TMP_73 \def (CHead TMP_71 TMP_72 u1) in (let TMP_74 \def 
+(CSort n) in (let TMP_75 \def (Bind b) in (let TMP_76 \def (CHead c2 TMP_75 
+u2) in (let TMP_77 \def (clear_gen_bind b0 TMP_74 TMP_76 u1 H0) in (let H3 
+\def (f_equal C T TMP_68 TMP_70 TMP_73 TMP_77) in (let TMP_170 \def (\lambda 
+(H4: (eq B b b0)).(\lambda (H5: (eq C c2 (CSort n))).(let TMP_78 \def (CSort 
+n) in (let TMP_95 \def (\lambda (c: C).(let TMP_81 \def (\lambda (e: C).(let 
+TMP_79 \def (Bind b0) in (let TMP_80 \def (CTail TMP_79 u1 e) in (eq C c 
+TMP_80)))) in (let TMP_85 \def (\lambda (e: C).(let TMP_82 \def (CSort n) in 
+(let TMP_83 \def (Bind b) in (let TMP_84 \def (CHead e TMP_83 u2) in (getl O 
+TMP_82 TMP_84))))) in (let TMP_86 \def (ex2 C TMP_81 TMP_85) in (let TMP_87 
+\def (\lambda (_: nat).(eq nat O O)) in (let TMP_90 \def (\lambda (_: 
+nat).(let TMP_88 \def (Bind b0) in (let TMP_89 \def (Bind b) in (eq K TMP_88 
+TMP_89)))) in (let TMP_91 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_93 
+\def (\lambda (n0: nat).(let TMP_92 \def (CSort n0) in (eq C c TMP_92))) in 
+(let TMP_94 \def (ex4 nat TMP_87 TMP_90 TMP_91 TMP_93) in (or TMP_86 
+TMP_94)))))))))) in (let TMP_114 \def (\lambda (t: T).(let TMP_99 \def 
+(\lambda (e: C).(let TMP_96 \def (CSort n) in (let TMP_97 \def (Bind b0) in 
+(let TMP_98 \def (CTail TMP_97 u1 e) in (eq C TMP_96 TMP_98))))) in (let 
+TMP_103 \def (\lambda (e: C).(let TMP_100 \def (CSort n) in (let TMP_101 \def 
+(Bind b) in (let TMP_102 \def (CHead e TMP_101 t) in (getl O TMP_100 
+TMP_102))))) in (let TMP_104 \def (ex2 C TMP_99 TMP_103) in (let TMP_105 \def 
+(\lambda (_: nat).(eq nat O O)) in (let TMP_108 \def (\lambda (_: nat).(let 
+TMP_106 \def (Bind b0) in (let TMP_107 \def (Bind b) in (eq K TMP_106 
+TMP_107)))) in (let TMP_109 \def (\lambda (_: nat).(eq T u1 t)) in (let 
+TMP_112 \def (\lambda (n0: nat).(let TMP_110 \def (CSort n) in (let TMP_111 
+\def (CSort n0) in (eq C TMP_110 TMP_111)))) in (let TMP_113 \def (ex4 nat 
+TMP_105 TMP_108 TMP_109 TMP_112) in (or TMP_104 TMP_113)))))))))) in (let 
+TMP_133 \def (\lambda (b1: B).(let TMP_118 \def (\lambda (e: C).(let TMP_115 
+\def (CSort n) in (let TMP_116 \def (Bind b0) in (let TMP_117 \def (CTail 
+TMP_116 u1 e) in (eq C TMP_115 TMP_117))))) in (let TMP_122 \def (\lambda (e: 
+C).(let TMP_119 \def (CSort n) in (let TMP_120 \def (Bind b1) in (let TMP_121 
+\def (CHead e TMP_120 u1) in (getl O TMP_119 TMP_121))))) in (let TMP_123 
+\def (ex2 C TMP_118 TMP_122) in (let TMP_124 \def (\lambda (_: nat).(eq nat O 
+O)) in (let TMP_127 \def (\lambda (_: nat).(let TMP_125 \def (Bind b0) in 
+(let TMP_126 \def (Bind b1) in (eq K TMP_125 TMP_126)))) in (let TMP_128 \def 
+(\lambda (_: nat).(eq T u1 u1)) in (let TMP_131 \def (\lambda (n0: nat).(let 
+TMP_129 \def (CSort n) in (let TMP_130 \def (CSort n0) in (eq C TMP_129 
+TMP_130)))) in (let TMP_132 \def (ex4 nat TMP_124 TMP_127 TMP_128 TMP_131) in 
+(or TMP_123 TMP_132)))))))))) in (let TMP_137 \def (\lambda (e: C).(let 
+TMP_134 \def (CSort n) in (let TMP_135 \def (Bind b0) in (let TMP_136 \def 
+(CTail TMP_135 u1 e) in (eq C TMP_134 TMP_136))))) in (let TMP_141 \def 
+(\lambda (e: C).(let TMP_138 \def (CSort n) in (let TMP_139 \def (Bind b0) in 
+(let TMP_140 \def (CHead e TMP_139 u1) in (getl O TMP_138 TMP_140))))) in 
+(let TMP_142 \def (ex2 C TMP_137 TMP_141) in (let TMP_143 \def (\lambda (_: 
+nat).(eq nat O O)) in (let TMP_146 \def (\lambda (_: nat).(let TMP_144 \def 
+(Bind b0) in (let TMP_145 \def (Bind b0) in (eq K TMP_144 TMP_145)))) in (let 
+TMP_147 \def (\lambda (_: nat).(eq T u1 u1)) in (let TMP_150 \def (\lambda 
+(n0: nat).(let TMP_148 \def (CSort n) in (let TMP_149 \def (CSort n0) in (eq 
+C TMP_148 TMP_149)))) in (let TMP_151 \def (ex4 nat TMP_143 TMP_146 TMP_147 
+TMP_150) in (let TMP_152 \def (\lambda (_: nat).(eq nat O O)) in (let TMP_155 
+\def (\lambda (_: nat).(let TMP_153 \def (Bind b0) in (let TMP_154 \def (Bind 
+b0) in (eq K TMP_153 TMP_154)))) in (let TMP_156 \def (\lambda (_: nat).(eq T 
+u1 u1)) in (let TMP_159 \def (\lambda (n0: nat).(let TMP_157 \def (CSort n) 
+in (let TMP_158 \def (CSort n0) in (eq C TMP_157 TMP_158)))) in (let TMP_160 
+\def (refl_equal nat O) in (let TMP_161 \def (Bind b0) in (let TMP_162 \def 
+(refl_equal K TMP_161) in (let TMP_163 \def (refl_equal T u1) in (let TMP_164 
+\def (CSort n) in (let TMP_165 \def (refl_equal C TMP_164) in (let TMP_166 
+\def (ex4_intro nat TMP_152 TMP_155 TMP_156 TMP_159 n TMP_160 TMP_162 TMP_163 
+TMP_165) in (let TMP_167 \def (or_intror TMP_142 TMP_151 TMP_166) in (let 
+TMP_168 \def (eq_ind_r B b0 TMP_133 TMP_167 b H4) in (let TMP_169 \def 
+(eq_ind_r T u1 TMP_114 TMP_168 u2 H3) in (eq_ind_r C TMP_78 TMP_95 TMP_169 c2 
+H5))))))))))))))))))))))))))))) in (let TMP_171 \def (TMP_170 H2) in (TMP_171 
+H1)))))))))))))))))))))))))))))))))))))) in (let TMP_196 \def (\lambda (f: 
+F).(\lambda (H0: (clear (CHead (CSort n) (Flat f) u1) (CHead c2 (Bind b) 
+u2))).(let TMP_173 \def (Bind b) in (let TMP_174 \def (CHead c2 TMP_173 u2) 
+in (let TMP_175 \def (CSort n) in (let TMP_176 \def (Bind b) in (let TMP_177 
+\def (CHead c2 TMP_176 u2) in (let TMP_178 \def (clear_gen_flat f TMP_175 
+TMP_177 u1 H0) in (let TMP_181 \def (\lambda (e: C).(let TMP_179 \def (Flat 
+f) in (let TMP_180 \def (CTail TMP_179 u1 e) in (eq C c2 TMP_180)))) in (let 
+TMP_185 \def (\lambda (e: C).(let TMP_182 \def (CSort n) in (let TMP_183 \def 
+(Bind b) in (let TMP_184 \def (CHead e TMP_183 u2) in (getl O TMP_182 
+TMP_184))))) in (let TMP_186 \def (ex2 C TMP_181 TMP_185) in (let TMP_187 
+\def (\lambda (_: nat).(eq nat O O)) in (let TMP_190 \def (\lambda (_: 
+nat).(let TMP_188 \def (Flat f) in (let TMP_189 \def (Bind b) in (eq K 
+TMP_188 TMP_189)))) in (let TMP_191 \def (\lambda (_: nat).(eq T u1 u2)) in 
+(let TMP_193 \def (\lambda (n0: nat).(let TMP_192 \def (CSort n0) in (eq C c2 
+TMP_192))) in (let TMP_194 \def (ex4 nat TMP_187 TMP_190 TMP_191 TMP_193) in 
+(let TMP_195 \def (or TMP_186 TMP_194) in (clear_gen_sort TMP_174 n TMP_178 
+TMP_195)))))))))))))))))) in (let TMP_197 \def (CSort n) in (let TMP_198 \def 
+(CHead TMP_197 k u1) in (let TMP_199 \def (Bind b) in (let TMP_200 \def 
+(CHead c2 TMP_199 u2) in (let TMP_201 \def (getl_gen_O TMP_198 TMP_200 H) in 
+(K_ind TMP_47 TMP_172 TMP_196 k TMP_201)))))))))) in (let TMP_227 \def 
+(\lambda (n0: nat).(\lambda (_: (((getl n0 (CHead (CSort n) k u1) (CHead c2 
 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) 
-(\lambda (e: C).(getl O (CHead c k1 t) (CHead e (Bind b) u2)))) (ex4 nat 
-(\lambda (_: nat).(eq nat O (s k1 (clen c)))) (\lambda (_: nat).(eq K k (Bind 
-b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort 
-n))))))) (\lambda (b0: B).(\lambda (H1: (clear (CHead (CTail k u1 c) (Bind 
-b0) t) (CHead c2 (Bind b) u2))).(let H2 \def (f_equal C C (\lambda (e: 
-C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | 
-(CHead c0 _ _) \Rightarrow c0])) (CHead c2 (Bind b) u2) (CHead (CTail k u1 c) 
-(Bind b0) t) (clear_gen_bind b0 (CTail k u1 c) (CHead c2 (Bind b) u2) t H1)) 
-in ((let H3 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda 
-(_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k1 _) \Rightarrow (match 
-k1 in K return (\lambda (_: K).B) with [(Bind b1) \Rightarrow b1 | (Flat _) 
-\Rightarrow b])])) (CHead c2 (Bind b) u2) (CHead (CTail k u1 c) (Bind b0) t) 
-(clear_gen_bind b0 (CTail k u1 c) (CHead c2 (Bind b) u2) t H1)) in ((let H4 
-\def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) 
-with [(CSort _) \Rightarrow u2 | (CHead _ _ t0) \Rightarrow t0])) (CHead c2 
-(Bind b) u2) (CHead (CTail k u1 c) (Bind b0) t) (clear_gen_bind b0 (CTail k 
-u1 c) (CHead c2 (Bind b) u2) t H1)) in (\lambda (H5: (eq B b b0)).(\lambda 
-(H6: (eq C c2 (CTail k u1 c))).(eq_ind T u2 (\lambda (t0: T).(or (ex2 C 
-(\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c 
-(Bind b0) t0) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O 
-(s (Bind b0) (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: 
-nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n)))))) (eq_ind B b 
-(\lambda (b1: B).(or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) 
-(\lambda (e: C).(getl O (CHead c (Bind b1) u2) (CHead e (Bind b) u2)))) (ex4 
-nat (\lambda (_: nat).(eq nat O (s (Bind b1) (clen c)))) (\lambda (_: 
-nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq 
-C c2 (CSort n)))))) (let H7 \def (eq_ind C c2 (\lambda (c0: C).(\forall (i0: 
-nat).((getl i0 (CTail k u1 c) (CHead c0 (Bind b) u2)) \to (or (ex2 C (\lambda 
-(e: C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl i0 c (CHead e (Bind b) 
-u2)))) (ex4 nat (\lambda (_: nat).(eq nat i0 (clen c))) (\lambda (_: nat).(eq 
-K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c0 
-(CSort n)))))))) H (CTail k u1 c) H6) in (eq_ind_r C (CTail k u1 c) (\lambda 
-(c0: C).(or (ex2 C (\lambda (e: C).(eq C c0 (CTail k u1 e))) (\lambda (e: 
-C).(getl O (CHead c (Bind b) u2) (CHead e (Bind b) u2)))) (ex4 nat (\lambda 
-(_: nat).(eq nat O (s (Bind b) (clen c)))) (\lambda (_: nat).(eq K k (Bind 
-b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c0 (CSort 
-n)))))) (or_introl (ex2 C (\lambda (e: C).(eq C (CTail k u1 c) (CTail k u1 
-e))) (\lambda (e: C).(getl O (CHead c (Bind b) u2) (CHead e (Bind b) u2)))) 
-(ex4 nat (\lambda (_: nat).(eq nat O (s (Bind b) (clen c)))) (\lambda (_: 
-nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq 
-C (CTail k u1 c) (CSort n)))) (ex_intro2 C (\lambda (e: C).(eq C (CTail k u1 
-c) (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Bind b) u2) (CHead e 
-(Bind b) u2))) c (refl_equal C (CTail k u1 c)) (getl_refl b c u2))) c2 H6)) 
-b0 H5) t H4)))) H3)) H2)))) (\lambda (f: F).(\lambda (H1: (clear (CHead 
-(CTail k u1 c) (Flat f) t) (CHead c2 (Bind b) u2))).(let H2 \def (H O 
-(getl_intro O (CTail k u1 c) (CHead c2 (Bind b) u2) (CTail k u1 c) (drop_refl 
-(CTail k u1 c)) (clear_gen_flat f (CTail k u1 c) (CHead c2 (Bind b) u2) t 
-H1))) in (or_ind (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda 
-(e: C).(getl O c (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat 
-O (clen c))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 
-u2)) (\lambda (n: nat).(eq C c2 (CSort n)))) (or (ex2 C (\lambda (e: C).(eq C 
-c2 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e 
-(Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) 
+(\lambda (e: C).(getl n0 (CSort n) (CHead e (Bind b) u2)))) (ex4 nat (\lambda 
+(_: nat).(eq nat n0 O)) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: 
+nat).(eq T u1 u2)) (\lambda (n1: nat).(eq C c2 (CSort n1)))))))).(\lambda 
+(H0: (getl (S n0) (CHead (CSort n) k u1) (CHead c2 (Bind b) u2))).(let 
+TMP_203 \def (r k n0) in (let TMP_204 \def (Bind b) in (let TMP_205 \def 
+(CHead c2 TMP_204 u2) in (let TMP_206 \def (CSort n) in (let TMP_207 \def 
+(Bind b) in (let TMP_208 \def (CHead c2 TMP_207 u2) in (let TMP_209 \def 
+(getl_gen_S k TMP_206 TMP_208 u1 n0 H0) in (let TMP_211 \def (\lambda (e: 
+C).(let TMP_210 \def (CTail k u1 e) in (eq C c2 TMP_210))) in (let TMP_216 
+\def (\lambda (e: C).(let TMP_212 \def (S n0) in (let TMP_213 \def (CSort n) 
+in (let TMP_214 \def (Bind b) in (let TMP_215 \def (CHead e TMP_214 u2) in 
+(getl TMP_212 TMP_213 TMP_215)))))) in (let TMP_217 \def (ex2 C TMP_211 
+TMP_216) in (let TMP_219 \def (\lambda (_: nat).(let TMP_218 \def (S n0) in 
+(eq nat TMP_218 O))) in (let TMP_221 \def (\lambda (_: nat).(let TMP_220 \def 
+(Bind b) in (eq K k TMP_220))) in (let TMP_222 \def (\lambda (_: nat).(eq T 
+u1 u2)) in (let TMP_224 \def (\lambda (n1: nat).(let TMP_223 \def (CSort n1) 
+in (eq C c2 TMP_223))) in (let TMP_225 \def (ex4 nat TMP_219 TMP_221 TMP_222 
+TMP_224) in (let TMP_226 \def (or TMP_217 TMP_225) in (getl_gen_sort n 
+TMP_203 TMP_205 TMP_209 TMP_226)))))))))))))))))))) in (nat_ind TMP_32 
+TMP_202 TMP_227 i)))))) in (let TMP_1086 \def (\lambda (c: C).(\lambda (H: 
+((\forall (i: nat).((getl i (CTail k u1 c) (CHead c2 (Bind b) u2)) \to (or 
+(ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl i c 
+(CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat i (clen c))) 
 (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda 
-(n: nat).(eq C c2 (CSort n))))) (\lambda (H3: (ex2 C (\lambda (e: C).(eq C c2 
-(CTail k u1 e))) (\lambda (e: C).(getl O c (CHead e (Bind b) u2))))).(ex2_ind 
-C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O c (CHead 
-e (Bind b) u2))) (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) 
-(\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)))) (ex4 
-nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) (\lambda (_: nat).(eq 
-K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 
-(CSort n))))) (\lambda (x: C).(\lambda (H4: (eq C c2 (CTail k u1 
-x))).(\lambda (H5: (getl O c (CHead x (Bind b) u2))).(eq_ind_r C (CTail k u1 
-x) (\lambda (c0: C).(or (ex2 C (\lambda (e: C).(eq C c0 (CTail k u1 e))) 
-(\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)))) (ex4 
-nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) (\lambda (_: nat).(eq 
-K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c0 
-(CSort n)))))) (or_introl (ex2 C (\lambda (e: C).(eq C (CTail k u1 x) (CTail 
-k u1 e))) (\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) 
-u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) (\lambda 
-(_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: 
-nat).(eq C (CTail k u1 x) (CSort n)))) (ex_intro2 C (\lambda (e: C).(eq C 
-(CTail k u1 x) (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Flat f) t) 
-(CHead e (Bind b) u2))) x (refl_equal C (CTail k u1 x)) (getl_flat c (CHead x 
-(Bind b) u2) O H5 f t))) c2 H4)))) H3)) (\lambda (H3: (ex4 nat (\lambda (_: 
+(n: nat).(eq C c2 (CSort n))))))))).(\lambda (k0: K).(\lambda (t: T).(\lambda 
+(i: nat).(let TMP_245 \def (\lambda (n: nat).((getl n (CTail k u1 (CHead c k0 
+t)) (CHead c2 (Bind b) u2)) \to (let TMP_230 \def (\lambda (e: C).(let 
+TMP_229 \def (CTail k u1 e) in (eq C c2 TMP_229))) in (let TMP_234 \def 
+(\lambda (e: C).(let TMP_231 \def (CHead c k0 t) in (let TMP_232 \def (Bind 
+b) in (let TMP_233 \def (CHead e TMP_232 u2) in (getl n TMP_231 TMP_233))))) 
+in (let TMP_235 \def (ex2 C TMP_230 TMP_234) in (let TMP_238 \def (\lambda 
+(_: nat).(let TMP_236 \def (CHead c k0 t) in (let TMP_237 \def (clen TMP_236) 
+in (eq nat n TMP_237)))) in (let TMP_240 \def (\lambda (_: nat).(let TMP_239 
+\def (Bind b) in (eq K k TMP_239))) in (let TMP_241 \def (\lambda (_: 
+nat).(eq T u1 u2)) in (let TMP_243 \def (\lambda (n0: nat).(let TMP_242 \def 
+(CSort n0) in (eq C c2 TMP_242))) in (let TMP_244 \def (ex4 nat TMP_238 
+TMP_240 TMP_241 TMP_243) in (or TMP_235 TMP_244))))))))))) in (let TMP_669 
+\def (\lambda (H0: (getl O (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) 
+u2))).(let TMP_262 \def (\lambda (k1: K).((clear (CHead (CTail k u1 c) k1 t) 
+(CHead c2 (Bind b) u2)) \to (let TMP_247 \def (\lambda (e: C).(let TMP_246 
+\def (CTail k u1 e) in (eq C c2 TMP_246))) in (let TMP_251 \def (\lambda (e: 
+C).(let TMP_248 \def (CHead c k1 t) in (let TMP_249 \def (Bind b) in (let 
+TMP_250 \def (CHead e TMP_249 u2) in (getl O TMP_248 TMP_250))))) in (let 
+TMP_252 \def (ex2 C TMP_247 TMP_251) in (let TMP_255 \def (\lambda (_: 
+nat).(let TMP_253 \def (clen c) in (let TMP_254 \def (s k1 TMP_253) in (eq 
+nat O TMP_254)))) in (let TMP_257 \def (\lambda (_: nat).(let TMP_256 \def 
+(Bind b) in (eq K k TMP_256))) in (let TMP_258 \def (\lambda (_: nat).(eq T 
+u1 u2)) in (let TMP_260 \def (\lambda (n: nat).(let TMP_259 \def (CSort n) in 
+(eq C c2 TMP_259))) in (let TMP_261 \def (ex4 nat TMP_255 TMP_257 TMP_258 
+TMP_260) in (or TMP_252 TMP_261))))))))))) in (let TMP_404 \def (\lambda (b0: 
+B).(\lambda (H1: (clear (CHead (CTail k u1 c) (Bind b0) t) (CHead c2 (Bind b) 
+u2))).(let TMP_263 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow 
+c2 | (CHead c0 _ _) \Rightarrow c0])) in (let TMP_264 \def (Bind b) in (let 
+TMP_265 \def (CHead c2 TMP_264 u2) in (let TMP_266 \def (CTail k u1 c) in 
+(let TMP_267 \def (Bind b0) in (let TMP_268 \def (CHead TMP_266 TMP_267 t) in 
+(let TMP_269 \def (CTail k u1 c) in (let TMP_270 \def (Bind b) in (let 
+TMP_271 \def (CHead c2 TMP_270 u2) in (let TMP_272 \def (clear_gen_bind b0 
+TMP_269 TMP_271 t H1) in (let H2 \def (f_equal C C TMP_263 TMP_265 TMP_268 
+TMP_272) in (let TMP_273 \def (\lambda (e: C).(match e with [(CSort _) 
+\Rightarrow b | (CHead _ k1 _) \Rightarrow (match k1 with [(Bind b1) 
+\Rightarrow b1 | (Flat _) \Rightarrow b])])) in (let TMP_274 \def (Bind b) in 
+(let TMP_275 \def (CHead c2 TMP_274 u2) in (let TMP_276 \def (CTail k u1 c) 
+in (let TMP_277 \def (Bind b0) in (let TMP_278 \def (CHead TMP_276 TMP_277 t) 
+in (let TMP_279 \def (CTail k u1 c) in (let TMP_280 \def (Bind b) in (let 
+TMP_281 \def (CHead c2 TMP_280 u2) in (let TMP_282 \def (clear_gen_bind b0 
+TMP_279 TMP_281 t H1) in (let H3 \def (f_equal C B TMP_273 TMP_275 TMP_278 
+TMP_282) in (let TMP_283 \def (\lambda (e: C).(match e with [(CSort _) 
+\Rightarrow u2 | (CHead _ _ t0) \Rightarrow t0])) in (let TMP_284 \def (Bind 
+b) in (let TMP_285 \def (CHead c2 TMP_284 u2) in (let TMP_286 \def (CTail k 
+u1 c) in (let TMP_287 \def (Bind b0) in (let TMP_288 \def (CHead TMP_286 
+TMP_287 t) in (let TMP_289 \def (CTail k u1 c) in (let TMP_290 \def (Bind b) 
+in (let TMP_291 \def (CHead c2 TMP_290 u2) in (let TMP_292 \def 
+(clear_gen_bind b0 TMP_289 TMP_291 t H1) in (let H4 \def (f_equal C T TMP_283 
+TMP_285 TMP_288 TMP_292) in (let TMP_402 \def (\lambda (H5: (eq B b 
+b0)).(\lambda (H6: (eq C c2 (CTail k u1 c))).(let TMP_311 \def (\lambda (t0: 
+T).(let TMP_294 \def (\lambda (e: C).(let TMP_293 \def (CTail k u1 e) in (eq 
+C c2 TMP_293))) in (let TMP_299 \def (\lambda (e: C).(let TMP_295 \def (Bind 
+b0) in (let TMP_296 \def (CHead c TMP_295 t0) in (let TMP_297 \def (Bind b) 
+in (let TMP_298 \def (CHead e TMP_297 u2) in (getl O TMP_296 TMP_298)))))) in 
+(let TMP_300 \def (ex2 C TMP_294 TMP_299) in (let TMP_304 \def (\lambda (_: 
+nat).(let TMP_301 \def (Bind b0) in (let TMP_302 \def (clen c) in (let 
+TMP_303 \def (s TMP_301 TMP_302) in (eq nat O TMP_303))))) in (let TMP_306 
+\def (\lambda (_: nat).(let TMP_305 \def (Bind b) in (eq K k TMP_305))) in 
+(let TMP_307 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_309 \def 
+(\lambda (n: nat).(let TMP_308 \def (CSort n) in (eq C c2 TMP_308))) in (let 
+TMP_310 \def (ex4 nat TMP_304 TMP_306 TMP_307 TMP_309) in (or TMP_300 
+TMP_310)))))))))) in (let TMP_330 \def (\lambda (b1: B).(let TMP_313 \def 
+(\lambda (e: C).(let TMP_312 \def (CTail k u1 e) in (eq C c2 TMP_312))) in 
+(let TMP_318 \def (\lambda (e: C).(let TMP_314 \def (Bind b1) in (let TMP_315 
+\def (CHead c TMP_314 u2) in (let TMP_316 \def (Bind b) in (let TMP_317 \def 
+(CHead e TMP_316 u2) in (getl O TMP_315 TMP_317)))))) in (let TMP_319 \def 
+(ex2 C TMP_313 TMP_318) in (let TMP_323 \def (\lambda (_: nat).(let TMP_320 
+\def (Bind b1) in (let TMP_321 \def (clen c) in (let TMP_322 \def (s TMP_320 
+TMP_321) in (eq nat O TMP_322))))) in (let TMP_325 \def (\lambda (_: 
+nat).(let TMP_324 \def (Bind b) in (eq K k TMP_324))) in (let TMP_326 \def 
+(\lambda (_: nat).(eq T u1 u2)) in (let TMP_328 \def (\lambda (n: nat).(let 
+TMP_327 \def (CSort n) in (eq C c2 TMP_327))) in (let TMP_329 \def (ex4 nat 
+TMP_323 TMP_325 TMP_326 TMP_328) in (or TMP_319 TMP_329)))))))))) in (let 
+TMP_345 \def (\lambda (c0: C).(\forall (i0: nat).((getl i0 (CTail k u1 c) 
+(CHead c0 (Bind b) u2)) \to (let TMP_332 \def (\lambda (e: C).(let TMP_331 
+\def (CTail k u1 e) in (eq C c0 TMP_331))) in (let TMP_335 \def (\lambda (e: 
+C).(let TMP_333 \def (Bind b) in (let TMP_334 \def (CHead e TMP_333 u2) in 
+(getl i0 c TMP_334)))) in (let TMP_336 \def (ex2 C TMP_332 TMP_335) in (let 
+TMP_338 \def (\lambda (_: nat).(let TMP_337 \def (clen c) in (eq nat i0 
+TMP_337))) in (let TMP_340 \def (\lambda (_: nat).(let TMP_339 \def (Bind b) 
+in (eq K k TMP_339))) in (let TMP_341 \def (\lambda (_: nat).(eq T u1 u2)) in 
+(let TMP_343 \def (\lambda (n: nat).(let TMP_342 \def (CSort n) in (eq C c0 
+TMP_342))) in (let TMP_344 \def (ex4 nat TMP_338 TMP_340 TMP_341 TMP_343) in 
+(or TMP_336 TMP_344)))))))))))) in (let TMP_346 \def (CTail k u1 c) in (let 
+H7 \def (eq_ind C c2 TMP_345 H TMP_346 H6) in (let TMP_347 \def (CTail k u1 
+c) in (let TMP_366 \def (\lambda (c0: C).(let TMP_349 \def (\lambda (e: 
+C).(let TMP_348 \def (CTail k u1 e) in (eq C c0 TMP_348))) in (let TMP_354 
+\def (\lambda (e: C).(let TMP_350 \def (Bind b) in (let TMP_351 \def (CHead c 
+TMP_350 u2) in (let TMP_352 \def (Bind b) in (let TMP_353 \def (CHead e 
+TMP_352 u2) in (getl O TMP_351 TMP_353)))))) in (let TMP_355 \def (ex2 C 
+TMP_349 TMP_354) in (let TMP_359 \def (\lambda (_: nat).(let TMP_356 \def 
+(Bind b) in (let TMP_357 \def (clen c) in (let TMP_358 \def (s TMP_356 
+TMP_357) in (eq nat O TMP_358))))) in (let TMP_361 \def (\lambda (_: 
+nat).(let TMP_360 \def (Bind b) in (eq K k TMP_360))) in (let TMP_362 \def 
+(\lambda (_: nat).(eq T u1 u2)) in (let TMP_364 \def (\lambda (n: nat).(let 
+TMP_363 \def (CSort n) in (eq C c0 TMP_363))) in (let TMP_365 \def (ex4 nat 
+TMP_359 TMP_361 TMP_362 TMP_364) in (or TMP_355 TMP_365)))))))))) in (let 
+TMP_369 \def (\lambda (e: C).(let TMP_367 \def (CTail k u1 c) in (let TMP_368 
+\def (CTail k u1 e) in (eq C TMP_367 TMP_368)))) in (let TMP_374 \def 
+(\lambda (e: C).(let TMP_370 \def (Bind b) in (let TMP_371 \def (CHead c 
+TMP_370 u2) in (let TMP_372 \def (Bind b) in (let TMP_373 \def (CHead e 
+TMP_372 u2) in (getl O TMP_371 TMP_373)))))) in (let TMP_375 \def (ex2 C 
+TMP_369 TMP_374) in (let TMP_379 \def (\lambda (_: nat).(let TMP_376 \def 
+(Bind b) in (let TMP_377 \def (clen c) in (let TMP_378 \def (s TMP_376 
+TMP_377) in (eq nat O TMP_378))))) in (let TMP_381 \def (\lambda (_: 
+nat).(let TMP_380 \def (Bind b) in (eq K k TMP_380))) in (let TMP_382 \def 
+(\lambda (_: nat).(eq T u1 u2)) in (let TMP_385 \def (\lambda (n: nat).(let 
+TMP_383 \def (CTail k u1 c) in (let TMP_384 \def (CSort n) in (eq C TMP_383 
+TMP_384)))) in (let TMP_386 \def (ex4 nat TMP_379 TMP_381 TMP_382 TMP_385) in 
+(let TMP_389 \def (\lambda (e: C).(let TMP_387 \def (CTail k u1 c) in (let 
+TMP_388 \def (CTail k u1 e) in (eq C TMP_387 TMP_388)))) in (let TMP_394 \def 
+(\lambda (e: C).(let TMP_390 \def (Bind b) in (let TMP_391 \def (CHead c 
+TMP_390 u2) in (let TMP_392 \def (Bind b) in (let TMP_393 \def (CHead e 
+TMP_392 u2) in (getl O TMP_391 TMP_393)))))) in (let TMP_395 \def (CTail k u1 
+c) in (let TMP_396 \def (refl_equal C TMP_395) in (let TMP_397 \def 
+(getl_refl b c u2) in (let TMP_398 \def (ex_intro2 C TMP_389 TMP_394 c 
+TMP_396 TMP_397) in (let TMP_399 \def (or_introl TMP_375 TMP_386 TMP_398) in 
+(let TMP_400 \def (eq_ind_r C TMP_347 TMP_366 TMP_399 c2 H6) in (let TMP_401 
+\def (eq_ind B b TMP_330 TMP_400 b0 H5) in (eq_ind T u2 TMP_311 TMP_401 t 
+H4))))))))))))))))))))))))))) in (let TMP_403 \def (TMP_402 H3) in (TMP_403 
+H2)))))))))))))))))))))))))))))))))))))) in (let TMP_663 \def (\lambda (f: 
+F).(\lambda (H1: (clear (CHead (CTail k u1 c) (Flat f) t) (CHead c2 (Bind b) 
+u2))).(let TMP_405 \def (CTail k u1 c) in (let TMP_406 \def (Bind b) in (let 
+TMP_407 \def (CHead c2 TMP_406 u2) in (let TMP_408 \def (CTail k u1 c) in 
+(let TMP_409 \def (CTail k u1 c) in (let TMP_410 \def (drop_refl TMP_409) in 
+(let TMP_411 \def (CTail k u1 c) in (let TMP_412 \def (Bind b) in (let 
+TMP_413 \def (CHead c2 TMP_412 u2) in (let TMP_414 \def (clear_gen_flat f 
+TMP_411 TMP_413 t H1) in (let TMP_415 \def (getl_intro O TMP_405 TMP_407 
+TMP_408 TMP_410 TMP_414) in (let H2 \def (H O TMP_415) in (let TMP_417 \def 
+(\lambda (e: C).(let TMP_416 \def (CTail k u1 e) in (eq C c2 TMP_416))) in 
+(let TMP_420 \def (\lambda (e: C).(let TMP_418 \def (Bind b) in (let TMP_419 
+\def (CHead e TMP_418 u2) in (getl O c TMP_419)))) in (let TMP_421 \def (ex2 
+C TMP_417 TMP_420) in (let TMP_423 \def (\lambda (_: nat).(let TMP_422 \def 
+(clen c) in (eq nat O TMP_422))) in (let TMP_425 \def (\lambda (_: nat).(let 
+TMP_424 \def (Bind b) in (eq K k TMP_424))) in (let TMP_426 \def (\lambda (_: 
+nat).(eq T u1 u2)) in (let TMP_428 \def (\lambda (n: nat).(let TMP_427 \def 
+(CSort n) in (eq C c2 TMP_427))) in (let TMP_429 \def (ex4 nat TMP_423 
+TMP_425 TMP_426 TMP_428) in (let TMP_431 \def (\lambda (e: C).(let TMP_430 
+\def (CTail k u1 e) in (eq C c2 TMP_430))) in (let TMP_436 \def (\lambda (e: 
+C).(let TMP_432 \def (Flat f) in (let TMP_433 \def (CHead c TMP_432 t) in 
+(let TMP_434 \def (Bind b) in (let TMP_435 \def (CHead e TMP_434 u2) in (getl 
+O TMP_433 TMP_435)))))) in (let TMP_437 \def (ex2 C TMP_431 TMP_436) in (let 
+TMP_441 \def (\lambda (_: nat).(let TMP_438 \def (Flat f) in (let TMP_439 
+\def (clen c) in (let TMP_440 \def (s TMP_438 TMP_439) in (eq nat O 
+TMP_440))))) in (let TMP_443 \def (\lambda (_: nat).(let TMP_442 \def (Bind 
+b) in (eq K k TMP_442))) in (let TMP_444 \def (\lambda (_: nat).(eq T u1 u2)) 
+in (let TMP_446 \def (\lambda (n: nat).(let TMP_445 \def (CSort n) in (eq C 
+c2 TMP_445))) in (let TMP_447 \def (ex4 nat TMP_441 TMP_443 TMP_444 TMP_446) 
+in (let TMP_448 \def (or TMP_437 TMP_447) in (let TMP_529 \def (\lambda (H3: 
+(ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O c 
+(CHead e (Bind b) u2))))).(let TMP_450 \def (\lambda (e: C).(let TMP_449 \def 
+(CTail k u1 e) in (eq C c2 TMP_449))) in (let TMP_453 \def (\lambda (e: 
+C).(let TMP_451 \def (Bind b) in (let TMP_452 \def (CHead e TMP_451 u2) in 
+(getl O c TMP_452)))) in (let TMP_455 \def (\lambda (e: C).(let TMP_454 \def 
+(CTail k u1 e) in (eq C c2 TMP_454))) in (let TMP_460 \def (\lambda (e: 
+C).(let TMP_456 \def (Flat f) in (let TMP_457 \def (CHead c TMP_456 t) in 
+(let TMP_458 \def (Bind b) in (let TMP_459 \def (CHead e TMP_458 u2) in (getl 
+O TMP_457 TMP_459)))))) in (let TMP_461 \def (ex2 C TMP_455 TMP_460) in (let 
+TMP_465 \def (\lambda (_: nat).(let TMP_462 \def (Flat f) in (let TMP_463 
+\def (clen c) in (let TMP_464 \def (s TMP_462 TMP_463) in (eq nat O 
+TMP_464))))) in (let TMP_467 \def (\lambda (_: nat).(let TMP_466 \def (Bind 
+b) in (eq K k TMP_466))) in (let TMP_468 \def (\lambda (_: nat).(eq T u1 u2)) 
+in (let TMP_470 \def (\lambda (n: nat).(let TMP_469 \def (CSort n) in (eq C 
+c2 TMP_469))) in (let TMP_471 \def (ex4 nat TMP_465 TMP_467 TMP_468 TMP_470) 
+in (let TMP_472 \def (or TMP_461 TMP_471) in (let TMP_528 \def (\lambda (x: 
+C).(\lambda (H4: (eq C c2 (CTail k u1 x))).(\lambda (H5: (getl O c (CHead x 
+(Bind b) u2))).(let TMP_473 \def (CTail k u1 x) in (let TMP_492 \def (\lambda 
+(c0: C).(let TMP_475 \def (\lambda (e: C).(let TMP_474 \def (CTail k u1 e) in 
+(eq C c0 TMP_474))) in (let TMP_480 \def (\lambda (e: C).(let TMP_476 \def 
+(Flat f) in (let TMP_477 \def (CHead c TMP_476 t) in (let TMP_478 \def (Bind 
+b) in (let TMP_479 \def (CHead e TMP_478 u2) in (getl O TMP_477 TMP_479)))))) 
+in (let TMP_481 \def (ex2 C TMP_475 TMP_480) in (let TMP_485 \def (\lambda 
+(_: nat).(let TMP_482 \def (Flat f) in (let TMP_483 \def (clen c) in (let 
+TMP_484 \def (s TMP_482 TMP_483) in (eq nat O TMP_484))))) in (let TMP_487 
+\def (\lambda (_: nat).(let TMP_486 \def (Bind b) in (eq K k TMP_486))) in 
+(let TMP_488 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_490 \def 
+(\lambda (n: nat).(let TMP_489 \def (CSort n) in (eq C c0 TMP_489))) in (let 
+TMP_491 \def (ex4 nat TMP_485 TMP_487 TMP_488 TMP_490) in (or TMP_481 
+TMP_491)))))))))) in (let TMP_495 \def (\lambda (e: C).(let TMP_493 \def 
+(CTail k u1 x) in (let TMP_494 \def (CTail k u1 e) in (eq C TMP_493 
+TMP_494)))) in (let TMP_500 \def (\lambda (e: C).(let TMP_496 \def (Flat f) 
+in (let TMP_497 \def (CHead c TMP_496 t) in (let TMP_498 \def (Bind b) in 
+(let TMP_499 \def (CHead e TMP_498 u2) in (getl O TMP_497 TMP_499)))))) in 
+(let TMP_501 \def (ex2 C TMP_495 TMP_500) in (let TMP_505 \def (\lambda (_: 
+nat).(let TMP_502 \def (Flat f) in (let TMP_503 \def (clen c) in (let TMP_504 
+\def (s TMP_502 TMP_503) in (eq nat O TMP_504))))) in (let TMP_507 \def 
+(\lambda (_: nat).(let TMP_506 \def (Bind b) in (eq K k TMP_506))) in (let 
+TMP_508 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_511 \def (\lambda 
+(n: nat).(let TMP_509 \def (CTail k u1 x) in (let TMP_510 \def (CSort n) in 
+(eq C TMP_509 TMP_510)))) in (let TMP_512 \def (ex4 nat TMP_505 TMP_507 
+TMP_508 TMP_511) in (let TMP_515 \def (\lambda (e: C).(let TMP_513 \def 
+(CTail k u1 x) in (let TMP_514 \def (CTail k u1 e) in (eq C TMP_513 
+TMP_514)))) in (let TMP_520 \def (\lambda (e: C).(let TMP_516 \def (Flat f) 
+in (let TMP_517 \def (CHead c TMP_516 t) in (let TMP_518 \def (Bind b) in 
+(let TMP_519 \def (CHead e TMP_518 u2) in (getl O TMP_517 TMP_519)))))) in 
+(let TMP_521 \def (CTail k u1 x) in (let TMP_522 \def (refl_equal C TMP_521) 
+in (let TMP_523 \def (Bind b) in (let TMP_524 \def (CHead x TMP_523 u2) in 
+(let TMP_525 \def (getl_flat c TMP_524 O H5 f t) in (let TMP_526 \def 
+(ex_intro2 C TMP_515 TMP_520 x TMP_522 TMP_525) in (let TMP_527 \def 
+(or_introl TMP_501 TMP_512 TMP_526) in (eq_ind_r C TMP_473 TMP_492 TMP_527 c2 
+H4))))))))))))))))))))))) in (ex2_ind C TMP_450 TMP_453 TMP_472 TMP_528 
+H3)))))))))))))) in (let TMP_662 \def (\lambda (H3: (ex4 nat (\lambda (_: 
 nat).(eq nat O (clen c))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: 
-nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))).(ex4_ind nat 
-(\lambda (_: nat).(eq nat O (clen c))) (\lambda (_: nat).(eq K k (Bind b))) 
-(\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n))) (or 
-(ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O 
-(CHead c (Flat f) t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq 
-nat O (s (Flat f) (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda 
-(_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))) (\lambda (x0: 
+nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))).(let TMP_531 \def 
+(\lambda (_: nat).(let TMP_530 \def (clen c) in (eq nat O TMP_530))) in (let 
+TMP_533 \def (\lambda (_: nat).(let TMP_532 \def (Bind b) in (eq K k 
+TMP_532))) in (let TMP_534 \def (\lambda (_: nat).(eq T u1 u2)) in (let 
+TMP_536 \def (\lambda (n: nat).(let TMP_535 \def (CSort n) in (eq C c2 
+TMP_535))) in (let TMP_538 \def (\lambda (e: C).(let TMP_537 \def (CTail k u1 
+e) in (eq C c2 TMP_537))) in (let TMP_543 \def (\lambda (e: C).(let TMP_539 
+\def (Flat f) in (let TMP_540 \def (CHead c TMP_539 t) in (let TMP_541 \def 
+(Bind b) in (let TMP_542 \def (CHead e TMP_541 u2) in (getl O TMP_540 
+TMP_542)))))) in (let TMP_544 \def (ex2 C TMP_538 TMP_543) in (let TMP_548 
+\def (\lambda (_: nat).(let TMP_545 \def (Flat f) in (let TMP_546 \def (clen 
+c) in (let TMP_547 \def (s TMP_545 TMP_546) in (eq nat O TMP_547))))) in (let 
+TMP_550 \def (\lambda (_: nat).(let TMP_549 \def (Bind b) in (eq K k 
+TMP_549))) in (let TMP_551 \def (\lambda (_: nat).(eq T u1 u2)) in (let 
+TMP_553 \def (\lambda (n: nat).(let TMP_552 \def (CSort n) in (eq C c2 
+TMP_552))) in (let TMP_554 \def (ex4 nat TMP_548 TMP_550 TMP_551 TMP_553) in 
+(let TMP_555 \def (or TMP_544 TMP_554) in (let TMP_661 \def (\lambda (x0: 
 nat).(\lambda (H4: (eq nat O (clen c))).(\lambda (H5: (eq K k (Bind 
-b))).(\lambda (H6: (eq T u1 u2)).(\lambda (H7: (eq C c2 (CSort 
-x0))).(eq_ind_r C (CSort x0) (\lambda (c0: C).(or (ex2 C (\lambda (e: C).(eq 
-C c0 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e 
-(Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) 
-(\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda 
-(n: nat).(eq C c0 (CSort n)))))) (eq_ind T u1 (\lambda (t0: T).(or (ex2 C 
-(\lambda (e: C).(eq C (CSort x0) (CTail k u1 e))) (\lambda (e: C).(getl O 
-(CHead c (Flat f) t) (CHead e (Bind b) t0)))) (ex4 nat (\lambda (_: nat).(eq 
-nat O (s (Flat f) (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda 
-(_: nat).(eq T u1 t0)) (\lambda (n: nat).(eq C (CSort x0) (CSort n)))))) 
-(eq_ind_r K (Bind b) (\lambda (k1: K).(or (ex2 C (\lambda (e: C).(eq C (CSort 
-x0) (CTail k1 u1 e))) (\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e 
-(Bind b) u1)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) 
-(\lambda (_: nat).(eq K k1 (Bind b))) (\lambda (_: nat).(eq T u1 u1)) 
-(\lambda (n: nat).(eq C (CSort x0) (CSort n)))))) (or_intror (ex2 C (\lambda 
-(e: C).(eq C (CSort x0) (CTail (Bind b) u1 e))) (\lambda (e: C).(getl O 
-(CHead c (Flat f) t) (CHead e (Bind b) u1)))) (ex4 nat (\lambda (_: nat).(eq 
-nat O (s (Flat f) (clen c)))) (\lambda (_: nat).(eq K (Bind b) (Bind b))) 
-(\lambda (_: nat).(eq T u1 u1)) (\lambda (n: nat).(eq C (CSort x0) (CSort 
-n)))) (ex4_intro nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) 
-(\lambda (_: nat).(eq K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1 u1)) 
-(\lambda (n: nat).(eq C (CSort x0) (CSort n))) x0 H4 (refl_equal K (Bind b)) 
-(refl_equal T u1) (refl_equal C (CSort x0)))) k H5) u2 H6) c2 H7)))))) H3)) 
-H2)))) k0 (getl_gen_O (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2) 
-H0))) (\lambda (n: nat).(\lambda (H0: (((getl n (CHead (CTail k u1 c) k0 t) 
-(CHead c2 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 
-e))) (\lambda (e: C).(getl n (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat 
-(\lambda (_: nat).(eq nat n (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind 
-b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort 
-n0)))))))).(\lambda (H1: (getl (S n) (CHead (CTail k u1 c) k0 t) (CHead c2 
-(Bind b) u2))).(let H_x \def (H (r k0 n) (getl_gen_S k0 (CTail k u1 c) (CHead 
-c2 (Bind b) u2) t n H1)) in (let H2 \def H_x in (or_ind (ex2 C (\lambda (e: 
-C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (r k0 n) c (CHead e (Bind 
-b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (r k0 n) (clen c))) (\lambda (_: 
-nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: 
-nat).(eq C c2 (CSort n0)))) (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 
-e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 
-nat (\lambda (_: nat).(eq nat (S n) (s k0 (clen c)))) (\lambda (_: nat).(eq K 
-k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 
-(CSort n0))))) (\lambda (H3: (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) 
-(\lambda (e: C).(getl (r k0 n) c (CHead e (Bind b) u2))))).(ex2_ind C 
-(\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (r k0 n) c 
-(CHead e (Bind b) u2))) (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) 
-(\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat 
-(\lambda (_: nat).(eq nat (S n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k 
-(Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort 
-n0))))) (\lambda (x: C).(\lambda (H4: (eq C c2 (CTail k u1 x))).(\lambda (H5: 
-(getl (r k0 n) c (CHead x (Bind b) u2))).(let H6 \def (eq_ind C c2 (\lambda 
-(c0: C).(getl (r k0 n) (CTail k u1 c) (CHead c0 (Bind b) u2))) (getl_gen_S k0 
-(CTail k u1 c) (CHead c2 (Bind b) u2) t n H1) (CTail k u1 x) H4) in (let H7 
-\def (eq_ind C c2 (\lambda (c0: C).((getl n (CHead (CTail k u1 c) k0 t) 
-(CHead c0 (Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c0 (CTail k u1 
-e))) (\lambda (e: C).(getl n (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat 
-(\lambda (_: nat).(eq nat n (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind 
-b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c0 (CSort 
-n0))))))) H0 (CTail k u1 x) H4) in (eq_ind_r C (CTail k u1 x) (\lambda (c0: 
-C).(or (ex2 C (\lambda (e: C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl 
-(S n) (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq 
-nat (S n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: 
-nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c0 (CSort n0)))))) (or_introl 
-(ex2 C (\lambda (e: C).(eq C (CTail k u1 x) (CTail k u1 e))) (\lambda (e: 
-C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: 
-nat).(eq nat (S n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) 
-(\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C (CTail k u1 x) 
-(CSort n0)))) (ex_intro2 C (\lambda (e: C).(eq C (CTail k u1 x) (CTail k u1 
-e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u2))) x 
-(refl_equal C (CTail k u1 x)) (getl_head k0 n c (CHead x (Bind b) u2) H5 t))) 
-c2 H4)))))) H3)) (\lambda (H3: (ex4 nat (\lambda (_: nat).(eq nat (r k0 n) 
-(clen c))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 
-u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))).(ex4_ind nat (\lambda (_: 
-nat).(eq nat (r k0 n) (clen c))) (\lambda (_: nat).(eq K k (Bind b))) 
-(\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))) (or 
-(ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (S n) 
-(CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S 
-n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: 
-nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))) (\lambda (x0: 
-nat).(\lambda (H4: (eq nat (r k0 n) (clen c))).(\lambda (H5: (eq K k (Bind 
-b))).(\lambda (H6: (eq T u1 u2)).(\lambda (H7: (eq C c2 (CSort x0))).(let H8 
-\def (eq_ind C c2 (\lambda (c0: C).(getl (r k0 n) (CTail k u1 c) (CHead c0 
-(Bind b) u2))) (getl_gen_S k0 (CTail k u1 c) (CHead c2 (Bind b) u2) t n H1) 
-(CSort x0) H7) in (let H9 \def (eq_ind C c2 (\lambda (c0: C).((getl n (CHead 
-(CTail k u1 c) k0 t) (CHead c0 (Bind b) u2)) \to (or (ex2 C (\lambda (e: 
-C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl n (CHead c k0 t) (CHead e 
-(Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat n (s k0 (clen c)))) 
-(\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda 
-(n0: nat).(eq C c0 (CSort n0))))))) H0 (CSort x0) H7) in (eq_ind_r C (CSort 
-x0) (\lambda (c0: C).(or (ex2 C (\lambda (e: C).(eq C c0 (CTail k u1 e))) 
-(\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4 nat 
-(\lambda (_: nat).(eq nat (S n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k 
-(Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c0 (CSort 
-n0)))))) (let H10 \def (eq_ind_r T u2 (\lambda (t0: T).((getl n (CHead (CTail 
-k u1 c) k0 t) (CHead (CSort x0) (Bind b) t0)) \to (or (ex2 C (\lambda (e: 
-C).(eq C (CSort x0) (CTail k u1 e))) (\lambda (e: C).(getl n (CHead c k0 t) 
-(CHead e (Bind b) t0)))) (ex4 nat (\lambda (_: nat).(eq nat n (s k0 (clen 
-c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 t0)) 
-(\lambda (n0: nat).(eq C (CSort x0) (CSort n0))))))) H9 u1 H6) in (let H11 
-\def (eq_ind_r T u2 (\lambda (t0: T).(getl (r k0 n) (CTail k u1 c) (CHead 
-(CSort x0) (Bind b) t0))) H8 u1 H6) in (eq_ind T u1 (\lambda (t0: T).(or (ex2 
-C (\lambda (e: C).(eq C (CSort x0) (CTail k u1 e))) (\lambda (e: C).(getl (S 
-n) (CHead c k0 t) (CHead e (Bind b) t0)))) (ex4 nat (\lambda (_: nat).(eq nat 
-(S n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: 
-nat).(eq T u1 t0)) (\lambda (n0: nat).(eq C (CSort x0) (CSort n0)))))) (let 
-H12 \def (eq_ind K k (\lambda (k1: K).((getl n (CHead (CTail k1 u1 c) k0 t) 
-(CHead (CSort x0) (Bind b) u1)) \to (or (ex2 C (\lambda (e: C).(eq C (CSort 
-x0) (CTail k1 u1 e))) (\lambda (e: C).(getl n (CHead c k0 t) (CHead e (Bind 
-b) u1)))) (ex4 nat (\lambda (_: nat).(eq nat n (s k0 (clen c)))) (\lambda (_: 
-nat).(eq K k1 (Bind b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n0: 
-nat).(eq C (CSort x0) (CSort n0))))))) H10 (Bind b) H5) in (let H13 \def 
-(eq_ind K k (\lambda (k1: K).(getl (r k0 n) (CTail k1 u1 c) (CHead (CSort x0) 
-(Bind b) u1))) H11 (Bind b) H5) in (eq_ind_r K (Bind b) (\lambda (k1: K).(or 
-(ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail k1 u1 e))) (\lambda (e: 
-C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)))) (ex4 nat (\lambda (_: 
-nat).(eq nat (S n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k1 (Bind b))) 
-(\lambda (_: nat).(eq T u1 u1)) (\lambda (n0: nat).(eq C (CSort x0) (CSort 
-n0)))))) (eq_ind nat (r k0 n) (\lambda (n0: nat).(or (ex2 C (\lambda (e: 
-C).(eq C (CSort x0) (CTail (Bind b) u1 e))) (\lambda (e: C).(getl (S n) 
-(CHead c k0 t) (CHead e (Bind b) u1)))) (ex4 nat (\lambda (_: nat).(eq nat (S 
-n) (s k0 n0))) (\lambda (_: nat).(eq K (Bind b) (Bind b))) (\lambda (_: 
-nat).(eq T u1 u1)) (\lambda (n1: nat).(eq C (CSort x0) (CSort n1)))))) 
-(eq_ind_r nat (S n) (\lambda (n0: nat).(or (ex2 C (\lambda (e: C).(eq C 
-(CSort x0) (CTail (Bind b) u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) 
-(CHead e (Bind b) u1)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) n0)) 
-(\lambda (_: nat).(eq K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1 u1)) 
-(\lambda (n1: nat).(eq C (CSort x0) (CSort n1)))))) (or_intror (ex2 C 
-(\lambda (e: C).(eq C (CSort x0) (CTail (Bind b) u1 e))) (\lambda (e: 
-C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)))) (ex4 nat (\lambda (_: 
-nat).(eq nat (S n) (S n))) (\lambda (_: nat).(eq K (Bind b) (Bind b))) 
-(\lambda (_: nat).(eq T u1 u1)) (\lambda (n0: nat).(eq C (CSort x0) (CSort 
-n0)))) (ex4_intro nat (\lambda (_: nat).(eq nat (S n) (S n))) (\lambda (_: 
-nat).(eq K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n0: 
-nat).(eq C (CSort x0) (CSort n0))) x0 (refl_equal nat (S n)) (refl_equal K 
-(Bind b)) (refl_equal T u1) (refl_equal C (CSort x0)))) (s k0 (r k0 n)) (s_r 
-k0 n)) (clen c) H4) k H5))) u2 H6))) c2 H7)))))))) H3)) H2)))))) i)))))) 
-c1)))))).
-(* COMMENTS
-Initial nodes: 7489
-END *)
+b))).(\lambda (H6: (eq T u1 u2)).(\lambda (H7: (eq C c2 (CSort x0))).(let 
+TMP_556 \def (CSort x0) in (let TMP_575 \def (\lambda (c0: C).(let TMP_558 
+\def (\lambda (e: C).(let TMP_557 \def (CTail k u1 e) in (eq C c0 TMP_557))) 
+in (let TMP_563 \def (\lambda (e: C).(let TMP_559 \def (Flat f) in (let 
+TMP_560 \def (CHead c TMP_559 t) in (let TMP_561 \def (Bind b) in (let 
+TMP_562 \def (CHead e TMP_561 u2) in (getl O TMP_560 TMP_562)))))) in (let 
+TMP_564 \def (ex2 C TMP_558 TMP_563) in (let TMP_568 \def (\lambda (_: 
+nat).(let TMP_565 \def (Flat f) in (let TMP_566 \def (clen c) in (let TMP_567 
+\def (s TMP_565 TMP_566) in (eq nat O TMP_567))))) in (let TMP_570 \def 
+(\lambda (_: nat).(let TMP_569 \def (Bind b) in (eq K k TMP_569))) in (let 
+TMP_571 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_573 \def (\lambda 
+(n: nat).(let TMP_572 \def (CSort n) in (eq C c0 TMP_572))) in (let TMP_574 
+\def (ex4 nat TMP_568 TMP_570 TMP_571 TMP_573) in (or TMP_564 
+TMP_574)))))))))) in (let TMP_596 \def (\lambda (t0: T).(let TMP_578 \def 
+(\lambda (e: C).(let TMP_576 \def (CSort x0) in (let TMP_577 \def (CTail k u1 
+e) in (eq C TMP_576 TMP_577)))) in (let TMP_583 \def (\lambda (e: C).(let 
+TMP_579 \def (Flat f) in (let TMP_580 \def (CHead c TMP_579 t) in (let 
+TMP_581 \def (Bind b) in (let TMP_582 \def (CHead e TMP_581 t0) in (getl O 
+TMP_580 TMP_582)))))) in (let TMP_584 \def (ex2 C TMP_578 TMP_583) in (let 
+TMP_588 \def (\lambda (_: nat).(let TMP_585 \def (Flat f) in (let TMP_586 
+\def (clen c) in (let TMP_587 \def (s TMP_585 TMP_586) in (eq nat O 
+TMP_587))))) in (let TMP_590 \def (\lambda (_: nat).(let TMP_589 \def (Bind 
+b) in (eq K k TMP_589))) in (let TMP_591 \def (\lambda (_: nat).(eq T u1 t0)) 
+in (let TMP_594 \def (\lambda (n: nat).(let TMP_592 \def (CSort x0) in (let 
+TMP_593 \def (CSort n) in (eq C TMP_592 TMP_593)))) in (let TMP_595 \def (ex4 
+nat TMP_588 TMP_590 TMP_591 TMP_594) in (or TMP_584 TMP_595)))))))))) in (let 
+TMP_597 \def (Bind b) in (let TMP_618 \def (\lambda (k1: K).(let TMP_600 \def 
+(\lambda (e: C).(let TMP_598 \def (CSort x0) in (let TMP_599 \def (CTail k1 
+u1 e) in (eq C TMP_598 TMP_599)))) in (let TMP_605 \def (\lambda (e: C).(let 
+TMP_601 \def (Flat f) in (let TMP_602 \def (CHead c TMP_601 t) in (let 
+TMP_603 \def (Bind b) in (let TMP_604 \def (CHead e TMP_603 u1) in (getl O 
+TMP_602 TMP_604)))))) in (let TMP_606 \def (ex2 C TMP_600 TMP_605) in (let 
+TMP_610 \def (\lambda (_: nat).(let TMP_607 \def (Flat f) in (let TMP_608 
+\def (clen c) in (let TMP_609 \def (s TMP_607 TMP_608) in (eq nat O 
+TMP_609))))) in (let TMP_612 \def (\lambda (_: nat).(let TMP_611 \def (Bind 
+b) in (eq K k1 TMP_611))) in (let TMP_613 \def (\lambda (_: nat).(eq T u1 
+u1)) in (let TMP_616 \def (\lambda (n: nat).(let TMP_614 \def (CSort x0) in 
+(let TMP_615 \def (CSort n) in (eq C TMP_614 TMP_615)))) in (let TMP_617 \def 
+(ex4 nat TMP_610 TMP_612 TMP_613 TMP_616) in (or TMP_606 TMP_617)))))))))) in 
+(let TMP_622 \def (\lambda (e: C).(let TMP_619 \def (CSort x0) in (let 
+TMP_620 \def (Bind b) in (let TMP_621 \def (CTail TMP_620 u1 e) in (eq C 
+TMP_619 TMP_621))))) in (let TMP_627 \def (\lambda (e: C).(let TMP_623 \def 
+(Flat f) in (let TMP_624 \def (CHead c TMP_623 t) in (let TMP_625 \def (Bind 
+b) in (let TMP_626 \def (CHead e TMP_625 u1) in (getl O TMP_624 TMP_626)))))) 
+in (let TMP_628 \def (ex2 C TMP_622 TMP_627) in (let TMP_632 \def (\lambda 
+(_: nat).(let TMP_629 \def (Flat f) in (let TMP_630 \def (clen c) in (let 
+TMP_631 \def (s TMP_629 TMP_630) in (eq nat O TMP_631))))) in (let TMP_635 
+\def (\lambda (_: nat).(let TMP_633 \def (Bind b) in (let TMP_634 \def (Bind 
+b) in (eq K TMP_633 TMP_634)))) in (let TMP_636 \def (\lambda (_: nat).(eq T 
+u1 u1)) in (let TMP_639 \def (\lambda (n: nat).(let TMP_637 \def (CSort x0) 
+in (let TMP_638 \def (CSort n) in (eq C TMP_637 TMP_638)))) in (let TMP_640 
+\def (ex4 nat TMP_632 TMP_635 TMP_636 TMP_639) in (let TMP_644 \def (\lambda 
+(_: nat).(let TMP_641 \def (Flat f) in (let TMP_642 \def (clen c) in (let 
+TMP_643 \def (s TMP_641 TMP_642) in (eq nat O TMP_643))))) in (let TMP_647 
+\def (\lambda (_: nat).(let TMP_645 \def (Bind b) in (let TMP_646 \def (Bind 
+b) in (eq K TMP_645 TMP_646)))) in (let TMP_648 \def (\lambda (_: nat).(eq T 
+u1 u1)) in (let TMP_651 \def (\lambda (n: nat).(let TMP_649 \def (CSort x0) 
+in (let TMP_650 \def (CSort n) in (eq C TMP_649 TMP_650)))) in (let TMP_652 
+\def (Bind b) in (let TMP_653 \def (refl_equal K TMP_652) in (let TMP_654 
+\def (refl_equal T u1) in (let TMP_655 \def (CSort x0) in (let TMP_656 \def 
+(refl_equal C TMP_655) in (let TMP_657 \def (ex4_intro nat TMP_644 TMP_647 
+TMP_648 TMP_651 x0 H4 TMP_653 TMP_654 TMP_656) in (let TMP_658 \def 
+(or_intror TMP_628 TMP_640 TMP_657) in (let TMP_659 \def (eq_ind_r K TMP_597 
+TMP_618 TMP_658 k H5) in (let TMP_660 \def (eq_ind T u1 TMP_596 TMP_659 u2 
+H6) in (eq_ind_r C TMP_556 TMP_575 TMP_660 c2 
+H7)))))))))))))))))))))))))))))))) in (ex4_ind nat TMP_531 TMP_533 TMP_534 
+TMP_536 TMP_555 TMP_661 H3)))))))))))))))) in (or_ind TMP_421 TMP_429 TMP_448 
+TMP_529 TMP_662 H2)))))))))))))))))))))))))))))))))) in (let TMP_664 \def 
+(CTail k u1 c) in (let TMP_665 \def (CHead TMP_664 k0 t) in (let TMP_666 \def 
+(Bind b) in (let TMP_667 \def (CHead c2 TMP_666 u2) in (let TMP_668 \def 
+(getl_gen_O TMP_665 TMP_667 H0) in (K_ind TMP_262 TMP_404 TMP_663 k0 
+TMP_668)))))))))) in (let TMP_1085 \def (\lambda (n: nat).(\lambda (H0: 
+(((getl n (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)) \to (or (ex2 C 
+(\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl n (CHead c k0 
+t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat n (s k0 (clen 
+c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) 
+(\lambda (n0: nat).(eq C c2 (CSort n0)))))))).(\lambda (H1: (getl (S n) 
+(CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2))).(let TMP_670 \def (r k0 
+n) in (let TMP_671 \def (CTail k u1 c) in (let TMP_672 \def (Bind b) in (let 
+TMP_673 \def (CHead c2 TMP_672 u2) in (let TMP_674 \def (getl_gen_S k0 
+TMP_671 TMP_673 t n H1) in (let H_x \def (H TMP_670 TMP_674) in (let H2 \def 
+H_x in (let TMP_676 \def (\lambda (e: C).(let TMP_675 \def (CTail k u1 e) in 
+(eq C c2 TMP_675))) in (let TMP_680 \def (\lambda (e: C).(let TMP_677 \def (r 
+k0 n) in (let TMP_678 \def (Bind b) in (let TMP_679 \def (CHead e TMP_678 u2) 
+in (getl TMP_677 c TMP_679))))) in (let TMP_681 \def (ex2 C TMP_676 TMP_680) 
+in (let TMP_684 \def (\lambda (_: nat).(let TMP_682 \def (r k0 n) in (let 
+TMP_683 \def (clen c) in (eq nat TMP_682 TMP_683)))) in (let TMP_686 \def 
+(\lambda (_: nat).(let TMP_685 \def (Bind b) in (eq K k TMP_685))) in (let 
+TMP_687 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_689 \def (\lambda 
+(n0: nat).(let TMP_688 \def (CSort n0) in (eq C c2 TMP_688))) in (let TMP_690 
+\def (ex4 nat TMP_684 TMP_686 TMP_687 TMP_689) in (let TMP_692 \def (\lambda 
+(e: C).(let TMP_691 \def (CTail k u1 e) in (eq C c2 TMP_691))) in (let 
+TMP_697 \def (\lambda (e: C).(let TMP_693 \def (S n) in (let TMP_694 \def 
+(CHead c k0 t) in (let TMP_695 \def (Bind b) in (let TMP_696 \def (CHead e 
+TMP_695 u2) in (getl TMP_693 TMP_694 TMP_696)))))) in (let TMP_698 \def (ex2 
+C TMP_692 TMP_697) in (let TMP_702 \def (\lambda (_: nat).(let TMP_699 \def 
+(S n) in (let TMP_700 \def (clen c) in (let TMP_701 \def (s k0 TMP_700) in 
+(eq nat TMP_699 TMP_701))))) in (let TMP_704 \def (\lambda (_: nat).(let 
+TMP_703 \def (Bind b) in (eq K k TMP_703))) in (let TMP_705 \def (\lambda (_: 
+nat).(eq T u1 u2)) in (let TMP_707 \def (\lambda (n0: nat).(let TMP_706 \def 
+(CSort n0) in (eq C c2 TMP_706))) in (let TMP_708 \def (ex4 nat TMP_702 
+TMP_704 TMP_705 TMP_707) in (let TMP_709 \def (or TMP_698 TMP_708) in (let 
+TMP_819 \def (\lambda (H3: (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) 
+(\lambda (e: C).(getl (r k0 n) c (CHead e (Bind b) u2))))).(let TMP_711 \def 
+(\lambda (e: C).(let TMP_710 \def (CTail k u1 e) in (eq C c2 TMP_710))) in 
+(let TMP_715 \def (\lambda (e: C).(let TMP_712 \def (r k0 n) in (let TMP_713 
+\def (Bind b) in (let TMP_714 \def (CHead e TMP_713 u2) in (getl TMP_712 c 
+TMP_714))))) in (let TMP_717 \def (\lambda (e: C).(let TMP_716 \def (CTail k 
+u1 e) in (eq C c2 TMP_716))) in (let TMP_722 \def (\lambda (e: C).(let 
+TMP_718 \def (S n) in (let TMP_719 \def (CHead c k0 t) in (let TMP_720 \def 
+(Bind b) in (let TMP_721 \def (CHead e TMP_720 u2) in (getl TMP_718 TMP_719 
+TMP_721)))))) in (let TMP_723 \def (ex2 C TMP_717 TMP_722) in (let TMP_727 
+\def (\lambda (_: nat).(let TMP_724 \def (S n) in (let TMP_725 \def (clen c) 
+in (let TMP_726 \def (s k0 TMP_725) in (eq nat TMP_724 TMP_726))))) in (let 
+TMP_729 \def (\lambda (_: nat).(let TMP_728 \def (Bind b) in (eq K k 
+TMP_728))) in (let TMP_730 \def (\lambda (_: nat).(eq T u1 u2)) in (let 
+TMP_732 \def (\lambda (n0: nat).(let TMP_731 \def (CSort n0) in (eq C c2 
+TMP_731))) in (let TMP_733 \def (ex4 nat TMP_727 TMP_729 TMP_730 TMP_732) in 
+(let TMP_734 \def (or TMP_723 TMP_733) in (let TMP_818 \def (\lambda (x: 
+C).(\lambda (H4: (eq C c2 (CTail k u1 x))).(\lambda (H5: (getl (r k0 n) c 
+(CHead x (Bind b) u2))).(let TMP_739 \def (\lambda (c0: C).(let TMP_735 \def 
+(r k0 n) in (let TMP_736 \def (CTail k u1 c) in (let TMP_737 \def (Bind b) in 
+(let TMP_738 \def (CHead c0 TMP_737 u2) in (getl TMP_735 TMP_736 
+TMP_738)))))) in (let TMP_740 \def (CTail k u1 c) in (let TMP_741 \def (Bind 
+b) in (let TMP_742 \def (CHead c2 TMP_741 u2) in (let TMP_743 \def 
+(getl_gen_S k0 TMP_740 TMP_742 t n H1) in (let TMP_744 \def (CTail k u1 x) in 
+(let H6 \def (eq_ind C c2 TMP_739 TMP_743 TMP_744 H4) in (let TMP_761 \def 
+(\lambda (c0: C).((getl n (CHead (CTail k u1 c) k0 t) (CHead c0 (Bind b) u2)) 
+\to (let TMP_746 \def (\lambda (e: C).(let TMP_745 \def (CTail k u1 e) in (eq 
+C c0 TMP_745))) in (let TMP_750 \def (\lambda (e: C).(let TMP_747 \def (CHead 
+c k0 t) in (let TMP_748 \def (Bind b) in (let TMP_749 \def (CHead e TMP_748 
+u2) in (getl n TMP_747 TMP_749))))) in (let TMP_751 \def (ex2 C TMP_746 
+TMP_750) in (let TMP_754 \def (\lambda (_: nat).(let TMP_752 \def (clen c) in 
+(let TMP_753 \def (s k0 TMP_752) in (eq nat n TMP_753)))) in (let TMP_756 
+\def (\lambda (_: nat).(let TMP_755 \def (Bind b) in (eq K k TMP_755))) in 
+(let TMP_757 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_759 \def 
+(\lambda (n0: nat).(let TMP_758 \def (CSort n0) in (eq C c0 TMP_758))) in 
+(let TMP_760 \def (ex4 nat TMP_754 TMP_756 TMP_757 TMP_759) in (or TMP_751 
+TMP_760))))))))))) in (let TMP_762 \def (CTail k u1 x) in (let H7 \def 
+(eq_ind C c2 TMP_761 H0 TMP_762 H4) in (let TMP_763 \def (CTail k u1 x) in 
+(let TMP_782 \def (\lambda (c0: C).(let TMP_765 \def (\lambda (e: C).(let 
+TMP_764 \def (CTail k u1 e) in (eq C c0 TMP_764))) in (let TMP_770 \def 
+(\lambda (e: C).(let TMP_766 \def (S n) in (let TMP_767 \def (CHead c k0 t) 
+in (let TMP_768 \def (Bind b) in (let TMP_769 \def (CHead e TMP_768 u2) in 
+(getl TMP_766 TMP_767 TMP_769)))))) in (let TMP_771 \def (ex2 C TMP_765 
+TMP_770) in (let TMP_775 \def (\lambda (_: nat).(let TMP_772 \def (S n) in 
+(let TMP_773 \def (clen c) in (let TMP_774 \def (s k0 TMP_773) in (eq nat 
+TMP_772 TMP_774))))) in (let TMP_777 \def (\lambda (_: nat).(let TMP_776 \def 
+(Bind b) in (eq K k TMP_776))) in (let TMP_778 \def (\lambda (_: nat).(eq T 
+u1 u2)) in (let TMP_780 \def (\lambda (n0: nat).(let TMP_779 \def (CSort n0) 
+in (eq C c0 TMP_779))) in (let TMP_781 \def (ex4 nat TMP_775 TMP_777 TMP_778 
+TMP_780) in (or TMP_771 TMP_781)))))))))) in (let TMP_785 \def (\lambda (e: 
+C).(let TMP_783 \def (CTail k u1 x) in (let TMP_784 \def (CTail k u1 e) in 
+(eq C TMP_783 TMP_784)))) in (let TMP_790 \def (\lambda (e: C).(let TMP_786 
+\def (S n) in (let TMP_787 \def (CHead c k0 t) in (let TMP_788 \def (Bind b) 
+in (let TMP_789 \def (CHead e TMP_788 u2) in (getl TMP_786 TMP_787 
+TMP_789)))))) in (let TMP_791 \def (ex2 C TMP_785 TMP_790) in (let TMP_795 
+\def (\lambda (_: nat).(let TMP_792 \def (S n) in (let TMP_793 \def (clen c) 
+in (let TMP_794 \def (s k0 TMP_793) in (eq nat TMP_792 TMP_794))))) in (let 
+TMP_797 \def (\lambda (_: nat).(let TMP_796 \def (Bind b) in (eq K k 
+TMP_796))) in (let TMP_798 \def (\lambda (_: nat).(eq T u1 u2)) in (let 
+TMP_801 \def (\lambda (n0: nat).(let TMP_799 \def (CTail k u1 x) in (let 
+TMP_800 \def (CSort n0) in (eq C TMP_799 TMP_800)))) in (let TMP_802 \def 
+(ex4 nat TMP_795 TMP_797 TMP_798 TMP_801) in (let TMP_805 \def (\lambda (e: 
+C).(let TMP_803 \def (CTail k u1 x) in (let TMP_804 \def (CTail k u1 e) in 
+(eq C TMP_803 TMP_804)))) in (let TMP_810 \def (\lambda (e: C).(let TMP_806 
+\def (S n) in (let TMP_807 \def (CHead c k0 t) in (let TMP_808 \def (Bind b) 
+in (let TMP_809 \def (CHead e TMP_808 u2) in (getl TMP_806 TMP_807 
+TMP_809)))))) in (let TMP_811 \def (CTail k u1 x) in (let TMP_812 \def 
+(refl_equal C TMP_811) in (let TMP_813 \def (Bind b) in (let TMP_814 \def 
+(CHead x TMP_813 u2) in (let TMP_815 \def (getl_head k0 n c TMP_814 H5 t) in 
+(let TMP_816 \def (ex_intro2 C TMP_805 TMP_810 x TMP_812 TMP_815) in (let 
+TMP_817 \def (or_introl TMP_791 TMP_802 TMP_816) in (eq_ind_r C TMP_763 
+TMP_782 TMP_817 c2 H4))))))))))))))))))))))))))))))))) in (ex2_ind C TMP_711 
+TMP_715 TMP_734 TMP_818 H3)))))))))))))) in (let TMP_1084 \def (\lambda (H3: 
+(ex4 nat (\lambda (_: nat).(eq nat (r k0 n) (clen c))) (\lambda (_: nat).(eq 
+K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 
+(CSort n0))))).(let TMP_822 \def (\lambda (_: nat).(let TMP_820 \def (r k0 n) 
+in (let TMP_821 \def (clen c) in (eq nat TMP_820 TMP_821)))) in (let TMP_824 
+\def (\lambda (_: nat).(let TMP_823 \def (Bind b) in (eq K k TMP_823))) in 
+(let TMP_825 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_827 \def 
+(\lambda (n0: nat).(let TMP_826 \def (CSort n0) in (eq C c2 TMP_826))) in 
+(let TMP_829 \def (\lambda (e: C).(let TMP_828 \def (CTail k u1 e) in (eq C 
+c2 TMP_828))) in (let TMP_834 \def (\lambda (e: C).(let TMP_830 \def (S n) in 
+(let TMP_831 \def (CHead c k0 t) in (let TMP_832 \def (Bind b) in (let 
+TMP_833 \def (CHead e TMP_832 u2) in (getl TMP_830 TMP_831 TMP_833)))))) in 
+(let TMP_835 \def (ex2 C TMP_829 TMP_834) in (let TMP_839 \def (\lambda (_: 
+nat).(let TMP_836 \def (S n) in (let TMP_837 \def (clen c) in (let TMP_838 
+\def (s k0 TMP_837) in (eq nat TMP_836 TMP_838))))) in (let TMP_841 \def 
+(\lambda (_: nat).(let TMP_840 \def (Bind b) in (eq K k TMP_840))) in (let 
+TMP_842 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_844 \def (\lambda 
+(n0: nat).(let TMP_843 \def (CSort n0) in (eq C c2 TMP_843))) in (let TMP_845 
+\def (ex4 nat TMP_839 TMP_841 TMP_842 TMP_844) in (let TMP_846 \def (or 
+TMP_835 TMP_845) in (let TMP_1083 \def (\lambda (x0: nat).(\lambda (H4: (eq 
+nat (r k0 n) (clen c))).(\lambda (H5: (eq K k (Bind b))).(\lambda (H6: (eq T 
+u1 u2)).(\lambda (H7: (eq C c2 (CSort x0))).(let TMP_851 \def (\lambda (c0: 
+C).(let TMP_847 \def (r k0 n) in (let TMP_848 \def (CTail k u1 c) in (let 
+TMP_849 \def (Bind b) in (let TMP_850 \def (CHead c0 TMP_849 u2) in (getl 
+TMP_847 TMP_848 TMP_850)))))) in (let TMP_852 \def (CTail k u1 c) in (let 
+TMP_853 \def (Bind b) in (let TMP_854 \def (CHead c2 TMP_853 u2) in (let 
+TMP_855 \def (getl_gen_S k0 TMP_852 TMP_854 t n H1) in (let TMP_856 \def 
+(CSort x0) in (let H8 \def (eq_ind C c2 TMP_851 TMP_855 TMP_856 H7) in (let 
+TMP_873 \def (\lambda (c0: C).((getl n (CHead (CTail k u1 c) k0 t) (CHead c0 
+(Bind b) u2)) \to (let TMP_858 \def (\lambda (e: C).(let TMP_857 \def (CTail 
+k u1 e) in (eq C c0 TMP_857))) in (let TMP_862 \def (\lambda (e: C).(let 
+TMP_859 \def (CHead c k0 t) in (let TMP_860 \def (Bind b) in (let TMP_861 
+\def (CHead e TMP_860 u2) in (getl n TMP_859 TMP_861))))) in (let TMP_863 
+\def (ex2 C TMP_858 TMP_862) in (let TMP_866 \def (\lambda (_: nat).(let 
+TMP_864 \def (clen c) in (let TMP_865 \def (s k0 TMP_864) in (eq nat n 
+TMP_865)))) in (let TMP_868 \def (\lambda (_: nat).(let TMP_867 \def (Bind b) 
+in (eq K k TMP_867))) in (let TMP_869 \def (\lambda (_: nat).(eq T u1 u2)) in 
+(let TMP_871 \def (\lambda (n0: nat).(let TMP_870 \def (CSort n0) in (eq C c0 
+TMP_870))) in (let TMP_872 \def (ex4 nat TMP_866 TMP_868 TMP_869 TMP_871) in 
+(or TMP_863 TMP_872))))))))))) in (let TMP_874 \def (CSort x0) in (let H9 
+\def (eq_ind C c2 TMP_873 H0 TMP_874 H7) in (let TMP_875 \def (CSort x0) in 
+(let TMP_894 \def (\lambda (c0: C).(let TMP_877 \def (\lambda (e: C).(let 
+TMP_876 \def (CTail k u1 e) in (eq C c0 TMP_876))) in (let TMP_882 \def 
+(\lambda (e: C).(let TMP_878 \def (S n) in (let TMP_879 \def (CHead c k0 t) 
+in (let TMP_880 \def (Bind b) in (let TMP_881 \def (CHead e TMP_880 u2) in 
+(getl TMP_878 TMP_879 TMP_881)))))) in (let TMP_883 \def (ex2 C TMP_877 
+TMP_882) in (let TMP_887 \def (\lambda (_: nat).(let TMP_884 \def (S n) in 
+(let TMP_885 \def (clen c) in (let TMP_886 \def (s k0 TMP_885) in (eq nat 
+TMP_884 TMP_886))))) in (let TMP_889 \def (\lambda (_: nat).(let TMP_888 \def 
+(Bind b) in (eq K k TMP_888))) in (let TMP_890 \def (\lambda (_: nat).(eq T 
+u1 u2)) in (let TMP_892 \def (\lambda (n0: nat).(let TMP_891 \def (CSort n0) 
+in (eq C c0 TMP_891))) in (let TMP_893 \def (ex4 nat TMP_887 TMP_889 TMP_890 
+TMP_892) in (or TMP_883 TMP_893)))))))))) in (let TMP_913 \def (\lambda (t0: 
+T).((getl n (CHead (CTail k u1 c) k0 t) (CHead (CSort x0) (Bind b) t0)) \to 
+(let TMP_897 \def (\lambda (e: C).(let TMP_895 \def (CSort x0) in (let 
+TMP_896 \def (CTail k u1 e) in (eq C TMP_895 TMP_896)))) in (let TMP_901 \def 
+(\lambda (e: C).(let TMP_898 \def (CHead c k0 t) in (let TMP_899 \def (Bind 
+b) in (let TMP_900 \def (CHead e TMP_899 t0) in (getl n TMP_898 TMP_900))))) 
+in (let TMP_902 \def (ex2 C TMP_897 TMP_901) in (let TMP_905 \def (\lambda 
+(_: nat).(let TMP_903 \def (clen c) in (let TMP_904 \def (s k0 TMP_903) in 
+(eq nat n TMP_904)))) in (let TMP_907 \def (\lambda (_: nat).(let TMP_906 
+\def (Bind b) in (eq K k TMP_906))) in (let TMP_908 \def (\lambda (_: 
+nat).(eq T u1 t0)) in (let TMP_911 \def (\lambda (n0: nat).(let TMP_909 \def 
+(CSort x0) in (let TMP_910 \def (CSort n0) in (eq C TMP_909 TMP_910)))) in 
+(let TMP_912 \def (ex4 nat TMP_905 TMP_907 TMP_908 TMP_911) in (or TMP_902 
+TMP_912))))))))))) in (let H10 \def (eq_ind_r T u2 TMP_913 H9 u1 H6) in (let 
+TMP_919 \def (\lambda (t0: T).(let TMP_914 \def (r k0 n) in (let TMP_915 \def 
+(CTail k u1 c) in (let TMP_916 \def (CSort x0) in (let TMP_917 \def (Bind b) 
+in (let TMP_918 \def (CHead TMP_916 TMP_917 t0) in (getl TMP_914 TMP_915 
+TMP_918))))))) in (let H11 \def (eq_ind_r T u2 TMP_919 H8 u1 H6) in (let 
+TMP_940 \def (\lambda (t0: T).(let TMP_922 \def (\lambda (e: C).(let TMP_920 
+\def (CSort x0) in (let TMP_921 \def (CTail k u1 e) in (eq C TMP_920 
+TMP_921)))) in (let TMP_927 \def (\lambda (e: C).(let TMP_923 \def (S n) in 
+(let TMP_924 \def (CHead c k0 t) in (let TMP_925 \def (Bind b) in (let 
+TMP_926 \def (CHead e TMP_925 t0) in (getl TMP_923 TMP_924 TMP_926)))))) in 
+(let TMP_928 \def (ex2 C TMP_922 TMP_927) in (let TMP_932 \def (\lambda (_: 
+nat).(let TMP_929 \def (S n) in (let TMP_930 \def (clen c) in (let TMP_931 
+\def (s k0 TMP_930) in (eq nat TMP_929 TMP_931))))) in (let TMP_934 \def 
+(\lambda (_: nat).(let TMP_933 \def (Bind b) in (eq K k TMP_933))) in (let 
+TMP_935 \def (\lambda (_: nat).(eq T u1 t0)) in (let TMP_938 \def (\lambda 
+(n0: nat).(let TMP_936 \def (CSort x0) in (let TMP_937 \def (CSort n0) in (eq 
+C TMP_936 TMP_937)))) in (let TMP_939 \def (ex4 nat TMP_932 TMP_934 TMP_935 
+TMP_938) in (or TMP_928 TMP_939)))))))))) in (let TMP_959 \def (\lambda (k1: 
+K).((getl n (CHead (CTail k1 u1 c) k0 t) (CHead (CSort x0) (Bind b) u1)) \to 
+(let TMP_943 \def (\lambda (e: C).(let TMP_941 \def (CSort x0) in (let 
+TMP_942 \def (CTail k1 u1 e) in (eq C TMP_941 TMP_942)))) in (let TMP_947 
+\def (\lambda (e: C).(let TMP_944 \def (CHead c k0 t) in (let TMP_945 \def 
+(Bind b) in (let TMP_946 \def (CHead e TMP_945 u1) in (getl n TMP_944 
+TMP_946))))) in (let TMP_948 \def (ex2 C TMP_943 TMP_947) in (let TMP_951 
+\def (\lambda (_: nat).(let TMP_949 \def (clen c) in (let TMP_950 \def (s k0 
+TMP_949) in (eq nat n TMP_950)))) in (let TMP_953 \def (\lambda (_: nat).(let 
+TMP_952 \def (Bind b) in (eq K k1 TMP_952))) in (let TMP_954 \def (\lambda 
+(_: nat).(eq T u1 u1)) in (let TMP_957 \def (\lambda (n0: nat).(let TMP_955 
+\def (CSort x0) in (let TMP_956 \def (CSort n0) in (eq C TMP_955 TMP_956)))) 
+in (let TMP_958 \def (ex4 nat TMP_951 TMP_953 TMP_954 TMP_957) in (or TMP_948 
+TMP_958))))))))))) in (let TMP_960 \def (Bind b) in (let H12 \def (eq_ind K k 
+TMP_959 H10 TMP_960 H5) in (let TMP_966 \def (\lambda (k1: K).(let TMP_961 
+\def (r k0 n) in (let TMP_962 \def (CTail k1 u1 c) in (let TMP_963 \def 
+(CSort x0) in (let TMP_964 \def (Bind b) in (let TMP_965 \def (CHead TMP_963 
+TMP_964 u1) in (getl TMP_961 TMP_962 TMP_965))))))) in (let TMP_967 \def 
+(Bind b) in (let H13 \def (eq_ind K k TMP_966 H11 TMP_967 H5) in (let TMP_968 
+\def (Bind b) in (let TMP_989 \def (\lambda (k1: K).(let TMP_971 \def 
+(\lambda (e: C).(let TMP_969 \def (CSort x0) in (let TMP_970 \def (CTail k1 
+u1 e) in (eq C TMP_969 TMP_970)))) in (let TMP_976 \def (\lambda (e: C).(let 
+TMP_972 \def (S n) in (let TMP_973 \def (CHead c k0 t) in (let TMP_974 \def 
+(Bind b) in (let TMP_975 \def (CHead e TMP_974 u1) in (getl TMP_972 TMP_973 
+TMP_975)))))) in (let TMP_977 \def (ex2 C TMP_971 TMP_976) in (let TMP_981 
+\def (\lambda (_: nat).(let TMP_978 \def (S n) in (let TMP_979 \def (clen c) 
+in (let TMP_980 \def (s k0 TMP_979) in (eq nat TMP_978 TMP_980))))) in (let 
+TMP_983 \def (\lambda (_: nat).(let TMP_982 \def (Bind b) in (eq K k1 
+TMP_982))) in (let TMP_984 \def (\lambda (_: nat).(eq T u1 u1)) in (let 
+TMP_987 \def (\lambda (n0: nat).(let TMP_985 \def (CSort x0) in (let TMP_986 
+\def (CSort n0) in (eq C TMP_985 TMP_986)))) in (let TMP_988 \def (ex4 nat 
+TMP_981 TMP_983 TMP_984 TMP_987) in (or TMP_977 TMP_988)))))))))) in (let 
+TMP_990 \def (r k0 n) in (let TMP_1012 \def (\lambda (n0: nat).(let TMP_994 
+\def (\lambda (e: C).(let TMP_991 \def (CSort x0) in (let TMP_992 \def (Bind 
+b) in (let TMP_993 \def (CTail TMP_992 u1 e) in (eq C TMP_991 TMP_993))))) in 
+(let TMP_999 \def (\lambda (e: C).(let TMP_995 \def (S n) in (let TMP_996 
+\def (CHead c k0 t) in (let TMP_997 \def (Bind b) in (let TMP_998 \def (CHead 
+e TMP_997 u1) in (getl TMP_995 TMP_996 TMP_998)))))) in (let TMP_1000 \def 
+(ex2 C TMP_994 TMP_999) in (let TMP_1003 \def (\lambda (_: nat).(let TMP_1001 
+\def (S n) in (let TMP_1002 \def (s k0 n0) in (eq nat TMP_1001 TMP_1002)))) 
+in (let TMP_1006 \def (\lambda (_: nat).(let TMP_1004 \def (Bind b) in (let 
+TMP_1005 \def (Bind b) in (eq K TMP_1004 TMP_1005)))) in (let TMP_1007 \def 
+(\lambda (_: nat).(eq T u1 u1)) in (let TMP_1010 \def (\lambda (n1: nat).(let 
+TMP_1008 \def (CSort x0) in (let TMP_1009 \def (CSort n1) in (eq C TMP_1008 
+TMP_1009)))) in (let TMP_1011 \def (ex4 nat TMP_1003 TMP_1006 TMP_1007 
+TMP_1010) in (or TMP_1000 TMP_1011)))))))))) in (let TMP_1013 \def (S n) in 
+(let TMP_1034 \def (\lambda (n0: nat).(let TMP_1017 \def (\lambda (e: C).(let 
+TMP_1014 \def (CSort x0) in (let TMP_1015 \def (Bind b) in (let TMP_1016 \def 
+(CTail TMP_1015 u1 e) in (eq C TMP_1014 TMP_1016))))) in (let TMP_1022 \def 
+(\lambda (e: C).(let TMP_1018 \def (S n) in (let TMP_1019 \def (CHead c k0 t) 
+in (let TMP_1020 \def (Bind b) in (let TMP_1021 \def (CHead e TMP_1020 u1) in 
+(getl TMP_1018 TMP_1019 TMP_1021)))))) in (let TMP_1023 \def (ex2 C TMP_1017 
+TMP_1022) in (let TMP_1025 \def (\lambda (_: nat).(let TMP_1024 \def (S n) in 
+(eq nat TMP_1024 n0))) in (let TMP_1028 \def (\lambda (_: nat).(let TMP_1026 
+\def (Bind b) in (let TMP_1027 \def (Bind b) in (eq K TMP_1026 TMP_1027)))) 
+in (let TMP_1029 \def (\lambda (_: nat).(eq T u1 u1)) in (let TMP_1032 \def 
+(\lambda (n1: nat).(let TMP_1030 \def (CSort x0) in (let TMP_1031 \def (CSort 
+n1) in (eq C TMP_1030 TMP_1031)))) in (let TMP_1033 \def (ex4 nat TMP_1025 
+TMP_1028 TMP_1029 TMP_1032) in (or TMP_1023 TMP_1033)))))))))) in (let 
+TMP_1038 \def (\lambda (e: C).(let TMP_1035 \def (CSort x0) in (let TMP_1036 
+\def (Bind b) in (let TMP_1037 \def (CTail TMP_1036 u1 e) in (eq C TMP_1035 
+TMP_1037))))) in (let TMP_1043 \def (\lambda (e: C).(let TMP_1039 \def (S n) 
+in (let TMP_1040 \def (CHead c k0 t) in (let TMP_1041 \def (Bind b) in (let 
+TMP_1042 \def (CHead e TMP_1041 u1) in (getl TMP_1039 TMP_1040 TMP_1042)))))) 
+in (let TMP_1044 \def (ex2 C TMP_1038 TMP_1043) in (let TMP_1047 \def 
+(\lambda (_: nat).(let TMP_1045 \def (S n) in (let TMP_1046 \def (S n) in (eq 
+nat TMP_1045 TMP_1046)))) in (let TMP_1050 \def (\lambda (_: nat).(let 
+TMP_1048 \def (Bind b) in (let TMP_1049 \def (Bind b) in (eq K TMP_1048 
+TMP_1049)))) in (let TMP_1051 \def (\lambda (_: nat).(eq T u1 u1)) in (let 
+TMP_1054 \def (\lambda (n0: nat).(let TMP_1052 \def (CSort x0) in (let 
+TMP_1053 \def (CSort n0) in (eq C TMP_1052 TMP_1053)))) in (let TMP_1055 \def 
+(ex4 nat TMP_1047 TMP_1050 TMP_1051 TMP_1054) in (let TMP_1058 \def (\lambda 
+(_: nat).(let TMP_1056 \def (S n) in (let TMP_1057 \def (S n) in (eq nat 
+TMP_1056 TMP_1057)))) in (let TMP_1061 \def (\lambda (_: nat).(let TMP_1059 
+\def (Bind b) in (let TMP_1060 \def (Bind b) in (eq K TMP_1059 TMP_1060)))) 
+in (let TMP_1062 \def (\lambda (_: nat).(eq T u1 u1)) in (let TMP_1065 \def 
+(\lambda (n0: nat).(let TMP_1063 \def (CSort x0) in (let TMP_1064 \def (CSort 
+n0) in (eq C TMP_1063 TMP_1064)))) in (let TMP_1066 \def (S n) in (let 
+TMP_1067 \def (refl_equal nat TMP_1066) in (let TMP_1068 \def (Bind b) in 
+(let TMP_1069 \def (refl_equal K TMP_1068) in (let TMP_1070 \def (refl_equal 
+T u1) in (let TMP_1071 \def (CSort x0) in (let TMP_1072 \def (refl_equal C 
+TMP_1071) in (let TMP_1073 \def (ex4_intro nat TMP_1058 TMP_1061 TMP_1062 
+TMP_1065 x0 TMP_1067 TMP_1069 TMP_1070 TMP_1072) in (let TMP_1074 \def 
+(or_intror TMP_1044 TMP_1055 TMP_1073) in (let TMP_1075 \def (r k0 n) in (let 
+TMP_1076 \def (s k0 TMP_1075) in (let TMP_1077 \def (s_r k0 n) in (let 
+TMP_1078 \def (eq_ind_r nat TMP_1013 TMP_1034 TMP_1074 TMP_1076 TMP_1077) in 
+(let TMP_1079 \def (clen c) in (let TMP_1080 \def (eq_ind nat TMP_990 
+TMP_1012 TMP_1078 TMP_1079 H4) in (let TMP_1081 \def (eq_ind_r K TMP_968 
+TMP_989 TMP_1080 k H5) in (let TMP_1082 \def (eq_ind T u1 TMP_940 TMP_1081 u2 
+H6) in (eq_ind_r C TMP_875 TMP_894 TMP_1082 c2 
+H7)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in 
+(ex4_ind nat TMP_822 TMP_824 TMP_825 TMP_827 TMP_846 TMP_1083 
+H3)))))))))))))))) in (or_ind TMP_681 TMP_690 TMP_709 TMP_819 TMP_1084 
+H2)))))))))))))))))))))))))))))) in (nat_ind TMP_245 TMP_669 TMP_1085 
+i))))))))) in (C_ind TMP_15 TMP_228 TMP_1086 c1))))))))).
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/drop1/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/drop1/defs.ma
index c0e14f438557bafbbd1d4a940da65c15773ddb77..c1953427f0e25bbec2fff160d5ca8dbd99e80fb0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/drop1/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/drop1/defs.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/drop/defs.ma".
+include "basic_1/drop/defs.ma".
 
-include "Basic-1/lift1/defs.ma".
+include "basic_1/lift1/defs.ma".
 
 inductive drop1: PList \to (C \to (C \to Prop)) \def
 | drop1_nil: \forall (c: C).(drop1 PNil c c)
@@ -24,12 +24,10 @@ inductive drop1: PList \to (C \to (C \to Prop)) \def
 nat).((drop h d c1 c2) \to (\forall (c3: C).(\forall (hds: PList).((drop1 hds 
 c2 c3) \to (drop1 (PCons h d hds) c1 c3)))))))).
 
-definition ptrans:
- PList \to (nat \to PList)
-\def
- let rec ptrans (hds: PList) on hds: (nat \to PList) \def (\lambda (i: 
+let rec ptrans (hds: PList) on hds: nat \to PList \def \lambda (i: 
 nat).(match hds with [PNil \Rightarrow PNil | (PCons h d hds0) \Rightarrow 
-(let j \def (trans hds0 i) in (let q \def (ptrans hds0 i) in (match (blt j d) 
-with [true \Rightarrow (PCons h (minus d (S j)) q) | false \Rightarrow 
-q])))])) in ptrans.
+(let j \def (trans hds0 i) in (let q \def (ptrans hds0 i) in (let TMP_1 \def 
+(blt j d) in (match TMP_1 with [true \Rightarrow (let TMP_2 \def (S j) in 
+(let TMP_3 \def (minus d TMP_2) in (PCons h TMP_3 q))) | false \Rightarrow 
+q]))))]).
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/drop1/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/drop1/fwd.ma
index 6e4d1789e832997e10cb8be5ae44488a6fdd0b68..606c71d8148ec7ca96d143ed0fe29cdee3515f5d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/drop1/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/drop1/fwd.ma
@@ -14,27 +14,35 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/drop1/defs.ma".
+include "basic_1/drop1/defs.ma".
+
+let rec drop1_ind (P: (PList \to (C \to (C \to Prop)))) (f: (\forall (c: 
+C).(P PNil c c))) (f0: (\forall (c1: C).(\forall (c2: C).(\forall (h: 
+nat).(\forall (d: nat).((drop h d c1 c2) \to (\forall (c3: C).(\forall (hds: 
+PList).((drop1 hds c2 c3) \to ((P hds c2 c3) \to (P (PCons h d hds) c1 
+c3))))))))))) (p: PList) (c: C) (c0: C) (d: drop1 p c c0) on d: P p c c0 \def 
+match d with [(drop1_nil c1) \Rightarrow (f c1) | (drop1_cons c1 c2 h d0 d1 
+c3 hds d2) \Rightarrow (let TMP_1 \def ((drop1_ind P f f0) hds c2 c3 d2) in 
+(f0 c1 c2 h d0 d1 c3 hds d2 TMP_1))].
 
 theorem drop1_gen_pnil:
  \forall (c1: C).(\forall (c2: C).((drop1 PNil c1 c2) \to (eq C c1 c2)))
 \def
- \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (drop1 PNil c1 c2)).(insert_eq 
-PList PNil (\lambda (p: PList).(drop1 p c1 c2)) (\lambda (_: PList).(eq C c1 
-c2)) (\lambda (y: PList).(\lambda (H0: (drop1 y c1 c2)).(drop1_ind (\lambda 
-(p: PList).(\lambda (c: C).(\lambda (c0: C).((eq PList p PNil) \to (eq C c 
-c0))))) (\lambda (c: C).(\lambda (_: (eq PList PNil PNil)).(refl_equal C c))) 
-(\lambda (c3: C).(\lambda (c4: C).(\lambda (h: nat).(\lambda (d: 
+ \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (drop1 PNil c1 c2)).(let TMP_1 
+\def (\lambda (p: PList).(drop1 p c1 c2)) in (let TMP_2 \def (\lambda (_: 
+PList).(eq C c1 c2)) in (let TMP_9 \def (\lambda (y: PList).(\lambda (H0: 
+(drop1 y c1 c2)).(let TMP_3 \def (\lambda (p: PList).(\lambda (c: C).(\lambda 
+(c0: C).((eq PList p PNil) \to (eq C c c0))))) in (let TMP_4 \def (\lambda 
+(c: C).(\lambda (_: (eq PList PNil PNil)).(refl_equal C c))) in (let TMP_8 
+\def (\lambda (c3: C).(\lambda (c4: C).(\lambda (h: nat).(\lambda (d: 
 nat).(\lambda (_: (drop h d c3 c4)).(\lambda (c5: C).(\lambda (hds: 
 PList).(\lambda (_: (drop1 hds c4 c5)).(\lambda (_: (((eq PList hds PNil) \to 
-(eq C c4 c5)))).(\lambda (H4: (eq PList (PCons h d hds) PNil)).(let H5 \def 
-(eq_ind PList (PCons h d hds) (\lambda (ee: PList).(match ee in PList return 
-(\lambda (_: PList).Prop) with [PNil \Rightarrow False | (PCons _ _ _) 
-\Rightarrow True])) I PNil H4) in (False_ind (eq C c3 c5) H5)))))))))))) y c1 
-c2 H0))) H))).
-(* COMMENTS
-Initial nodes: 198
-END *)
+(eq C c4 c5)))).(\lambda (H4: (eq PList (PCons h d hds) PNil)).(let TMP_5 
+\def (PCons h d hds) in (let TMP_6 \def (\lambda (ee: PList).(match ee with 
+[PNil \Rightarrow False | (PCons _ _ _) \Rightarrow True])) in (let H5 \def 
+(eq_ind PList TMP_5 TMP_6 I PNil H4) in (let TMP_7 \def (eq C c3 c5) in 
+(False_ind TMP_7 H5))))))))))))))) in (drop1_ind TMP_3 TMP_4 TMP_8 y c1 c2 
+H0)))))) in (insert_eq PList PNil TMP_1 TMP_2 TMP_9 H)))))).
 
 theorem drop1_gen_pcons:
  \forall (c1: C).(\forall (c3: C).(\forall (hds: PList).(\forall (h: 
@@ -42,40 +50,47 @@ nat).(\forall (d: nat).((drop1 (PCons h d hds) c1 c3) \to (ex2 C (\lambda
 (c2: C).(drop h d c1 c2)) (\lambda (c2: C).(drop1 hds c2 c3))))))))
 \def
  \lambda (c1: C).(\lambda (c3: C).(\lambda (hds: PList).(\lambda (h: 
-nat).(\lambda (d: nat).(\lambda (H: (drop1 (PCons h d hds) c1 c3)).(insert_eq 
-PList (PCons h d hds) (\lambda (p: PList).(drop1 p c1 c3)) (\lambda (_: 
-PList).(ex2 C (\lambda (c2: C).(drop h d c1 c2)) (\lambda (c2: C).(drop1 hds 
-c2 c3)))) (\lambda (y: PList).(\lambda (H0: (drop1 y c1 c3)).(drop1_ind 
-(\lambda (p: PList).(\lambda (c: C).(\lambda (c0: C).((eq PList p (PCons h d 
-hds)) \to (ex2 C (\lambda (c2: C).(drop h d c c2)) (\lambda (c2: C).(drop1 
-hds c2 c0))))))) (\lambda (c: C).(\lambda (H1: (eq PList PNil (PCons h d 
-hds))).(let H2 \def (eq_ind PList PNil (\lambda (ee: PList).(match ee in 
-PList return (\lambda (_: PList).Prop) with [PNil \Rightarrow True | (PCons _ 
-_ _) \Rightarrow False])) I (PCons h d hds) H1) in (False_ind (ex2 C (\lambda 
-(c2: C).(drop h d c c2)) (\lambda (c2: C).(drop1 hds c2 c))) H2)))) (\lambda 
-(c2: C).(\lambda (c4: C).(\lambda (h0: nat).(\lambda (d0: nat).(\lambda (H1: 
-(drop h0 d0 c2 c4)).(\lambda (c5: C).(\lambda (hds0: PList).(\lambda (H2: 
-(drop1 hds0 c4 c5)).(\lambda (H3: (((eq PList hds0 (PCons h d hds)) \to (ex2 
-C (\lambda (c6: C).(drop h d c4 c6)) (\lambda (c6: C).(drop1 hds c6 
-c5)))))).(\lambda (H4: (eq PList (PCons h0 d0 hds0) (PCons h d hds))).(let H5 
-\def (f_equal PList nat (\lambda (e: PList).(match e in PList return (\lambda 
-(_: PList).nat) with [PNil \Rightarrow h0 | (PCons n _ _) \Rightarrow n])) 
-(PCons h0 d0 hds0) (PCons h d hds) H4) in ((let H6 \def (f_equal PList nat 
-(\lambda (e: PList).(match e in PList return (\lambda (_: PList).nat) with 
-[PNil \Rightarrow d0 | (PCons _ n _) \Rightarrow n])) (PCons h0 d0 hds0) 
-(PCons h d hds) H4) in ((let H7 \def (f_equal PList PList (\lambda (e: 
-PList).(match e in PList return (\lambda (_: PList).PList) with [PNil 
-\Rightarrow hds0 | (PCons _ _ p) \Rightarrow p])) (PCons h0 d0 hds0) (PCons h 
-d hds) H4) in (\lambda (H8: (eq nat d0 d)).(\lambda (H9: (eq nat h0 h)).(let 
-H10 \def (eq_ind PList hds0 (\lambda (p: PList).((eq PList p (PCons h d hds)) 
-\to (ex2 C (\lambda (c6: C).(drop h d c4 c6)) (\lambda (c6: C).(drop1 hds c6 
-c5))))) H3 hds H7) in (let H11 \def (eq_ind PList hds0 (\lambda (p: 
-PList).(drop1 p c4 c5)) H2 hds H7) in (let H12 \def (eq_ind nat d0 (\lambda 
-(n: nat).(drop h0 n c2 c4)) H1 d H8) in (let H13 \def (eq_ind nat h0 (\lambda 
-(n: nat).(drop n d c2 c4)) H12 h H9) in (ex_intro2 C (\lambda (c6: C).(drop h 
-d c2 c6)) (\lambda (c6: C).(drop1 hds c6 c5)) c4 H13 H11)))))))) H6)) 
-H5)))))))))))) y c1 c3 H0))) H)))))).
-(* COMMENTS
-Initial nodes: 587
-END *)
+nat).(\lambda (d: nat).(\lambda (H: (drop1 (PCons h d hds) c1 c3)).(let TMP_1 
+\def (PCons h d hds) in (let TMP_2 \def (\lambda (p: PList).(drop1 p c1 c3)) 
+in (let TMP_5 \def (\lambda (_: PList).(let TMP_3 \def (\lambda (c2: C).(drop 
+h d c1 c2)) in (let TMP_4 \def (\lambda (c2: C).(drop1 hds c2 c3)) in (ex2 C 
+TMP_3 TMP_4)))) in (let TMP_35 \def (\lambda (y: PList).(\lambda (H0: (drop1 
+y c1 c3)).(let TMP_8 \def (\lambda (p: PList).(\lambda (c: C).(\lambda (c0: 
+C).((eq PList p (PCons h d hds)) \to (let TMP_6 \def (\lambda (c2: C).(drop h 
+d c c2)) in (let TMP_7 \def (\lambda (c2: C).(drop1 hds c2 c0)) in (ex2 C 
+TMP_6 TMP_7))))))) in (let TMP_14 \def (\lambda (c: C).(\lambda (H1: (eq 
+PList PNil (PCons h d hds))).(let TMP_9 \def (\lambda (ee: PList).(match ee 
+with [PNil \Rightarrow True | (PCons _ _ _) \Rightarrow False])) in (let 
+TMP_10 \def (PCons h d hds) in (let H2 \def (eq_ind PList PNil TMP_9 I TMP_10 
+H1) in (let TMP_11 \def (\lambda (c2: C).(drop h d c c2)) in (let TMP_12 \def 
+(\lambda (c2: C).(drop1 hds c2 c)) in (let TMP_13 \def (ex2 C TMP_11 TMP_12) 
+in (False_ind TMP_13 H2))))))))) in (let TMP_34 \def (\lambda (c2: 
+C).(\lambda (c4: C).(\lambda (h0: nat).(\lambda (d0: nat).(\lambda (H1: (drop 
+h0 d0 c2 c4)).(\lambda (c5: C).(\lambda (hds0: PList).(\lambda (H2: (drop1 
+hds0 c4 c5)).(\lambda (H3: (((eq PList hds0 (PCons h d hds)) \to (ex2 C 
+(\lambda (c6: C).(drop h d c4 c6)) (\lambda (c6: C).(drop1 hds c6 
+c5)))))).(\lambda (H4: (eq PList (PCons h0 d0 hds0) (PCons h d hds))).(let 
+TMP_15 \def (\lambda (e: PList).(match e with [PNil \Rightarrow h0 | (PCons n 
+_ _) \Rightarrow n])) in (let TMP_16 \def (PCons h0 d0 hds0) in (let TMP_17 
+\def (PCons h d hds) in (let H5 \def (f_equal PList nat TMP_15 TMP_16 TMP_17 
+H4) in (let TMP_18 \def (\lambda (e: PList).(match e with [PNil \Rightarrow 
+d0 | (PCons _ n _) \Rightarrow n])) in (let TMP_19 \def (PCons h0 d0 hds0) in 
+(let TMP_20 \def (PCons h d hds) in (let H6 \def (f_equal PList nat TMP_18 
+TMP_19 TMP_20 H4) in (let TMP_21 \def (\lambda (e: PList).(match e with [PNil 
+\Rightarrow hds0 | (PCons _ _ p) \Rightarrow p])) in (let TMP_22 \def (PCons 
+h0 d0 hds0) in (let TMP_23 \def (PCons h d hds) in (let H7 \def (f_equal 
+PList PList TMP_21 TMP_22 TMP_23 H4) in (let TMP_32 \def (\lambda (H8: (eq 
+nat d0 d)).(\lambda (H9: (eq nat h0 h)).(let TMP_26 \def (\lambda (p: 
+PList).((eq PList p (PCons h d hds)) \to (let TMP_24 \def (\lambda (c6: 
+C).(drop h d c4 c6)) in (let TMP_25 \def (\lambda (c6: C).(drop1 hds c6 c5)) 
+in (ex2 C TMP_24 TMP_25))))) in (let H10 \def (eq_ind PList hds0 TMP_26 H3 
+hds H7) in (let TMP_27 \def (\lambda (p: PList).(drop1 p c4 c5)) in (let H11 
+\def (eq_ind PList hds0 TMP_27 H2 hds H7) in (let TMP_28 \def (\lambda (n: 
+nat).(drop h0 n c2 c4)) in (let H12 \def (eq_ind nat d0 TMP_28 H1 d H8) in 
+(let TMP_29 \def (\lambda (n: nat).(drop n d c2 c4)) in (let H13 \def (eq_ind 
+nat h0 TMP_29 H12 h H9) in (let TMP_30 \def (\lambda (c6: C).(drop h d c2 
+c6)) in (let TMP_31 \def (\lambda (c6: C).(drop1 hds c6 c5)) in (ex_intro2 C 
+TMP_30 TMP_31 c4 H13 H11))))))))))))) in (let TMP_33 \def (TMP_32 H6) in 
+(TMP_33 H5))))))))))))))))))))))))) in (drop1_ind TMP_8 TMP_14 TMP_34 y c1 c3 
+H0)))))) in (insert_eq PList TMP_1 TMP_2 TMP_5 TMP_35 H)))))))))).
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/drop1/getl.ma b/matita/matita/contribs/lambdadelta/basic_1/drop1/getl.ma
index dbee798509f2bad6d663a3f85a8f25d16c6f845c..6d790740689c569a00f8c83bfd218672e79f825b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/drop1/getl.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/drop1/getl.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/drop1/fwd.ma".
+include "basic_1/drop1/fwd.ma".
 
-include "Basic-1/getl/drop.ma".
+include "basic_1/getl/drop.ma".
 
 theorem drop1_getl_trans:
  \forall (hds: PList).(\forall (c1: C).(\forall (c2: C).((drop1 hds c2 c1) 
@@ -25,86 +25,165 @@ i c1 (CHead e1 (Bind b) v)) \to (ex2 C (\lambda (e2: C).(drop1 (ptrans hds i)
 e2 e1)) (\lambda (e2: C).(getl (trans hds i) c2 (CHead e2 (Bind b) (lift1 
 (ptrans hds i) v)))))))))))))
 \def
- \lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (c1: 
+ \lambda (hds: PList).(let TMP_9 \def (\lambda (p: PList).(\forall (c1: 
 C).(\forall (c2: C).((drop1 p c2 c1) \to (\forall (b: B).(\forall (e1: 
 C).(\forall (v: T).(\forall (i: nat).((getl i c1 (CHead e1 (Bind b) v)) \to 
-(ex2 C (\lambda (e2: C).(drop1 (ptrans p i) e2 e1)) (\lambda (e2: C).(getl 
-(trans p i) c2 (CHead e2 (Bind b) (lift1 (ptrans p i) v)))))))))))))) 
-(\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (drop1 PNil c2 c1)).(\lambda 
-(b: B).(\lambda (e1: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H0: (getl 
-i c1 (CHead e1 (Bind b) v))).(let H_y \def (drop1_gen_pnil c2 c1 H) in 
-(eq_ind_r C c1 (\lambda (c: C).(ex2 C (\lambda (e2: C).(drop1 PNil e2 e1)) 
-(\lambda (e2: C).(getl i c (CHead e2 (Bind b) v))))) (ex_intro2 C (\lambda 
-(e2: C).(drop1 PNil e2 e1)) (\lambda (e2: C).(getl i c1 (CHead e2 (Bind b) 
-v))) e1 (drop1_nil e1) H0) c2 H_y)))))))))) (\lambda (h: nat).(\lambda (d: 
-nat).(\lambda (hds0: PList).(\lambda (H: ((\forall (c1: C).(\forall (c2: 
-C).((drop1 hds0 c2 c1) \to (\forall (b: B).(\forall (e1: C).(\forall (v: 
-T).(\forall (i: nat).((getl i c1 (CHead e1 (Bind b) v)) \to (ex2 C (\lambda 
-(e2: C).(drop1 (ptrans hds0 i) e2 e1)) (\lambda (e2: C).(getl (trans hds0 i) 
-c2 (CHead e2 (Bind b) (lift1 (ptrans hds0 i) v))))))))))))))).(\lambda (c1: 
-C).(\lambda (c2: C).(\lambda (H0: (drop1 (PCons h d hds0) c2 c1)).(\lambda 
-(b: B).(\lambda (e1: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H1: (getl 
-i c1 (CHead e1 (Bind b) v))).(let H_x \def (drop1_gen_pcons c2 c1 hds0 h d 
-H0) in (let H2 \def H_x in (ex2_ind C (\lambda (c3: C).(drop h d c2 c3)) 
-(\lambda (c3: C).(drop1 hds0 c3 c1)) (ex2 C (\lambda (e2: C).(drop1 (match 
-(blt (trans hds0 i) d) with [true \Rightarrow (PCons h (minus d (S (trans 
-hds0 i))) (ptrans hds0 i)) | false \Rightarrow (ptrans hds0 i)]) e2 e1)) 
-(\lambda (e2: C).(getl (match (blt (trans hds0 i) d) with [true \Rightarrow 
-(trans hds0 i) | false \Rightarrow (plus (trans hds0 i) h)]) c2 (CHead e2 
-(Bind b) (lift1 (match (blt (trans hds0 i) d) with [true \Rightarrow (PCons h 
-(minus d (S (trans hds0 i))) (ptrans hds0 i)) | false \Rightarrow (ptrans 
-hds0 i)]) v))))) (\lambda (x: C).(\lambda (H3: (drop h d c2 x)).(\lambda (H4: 
-(drop1 hds0 x c1)).(xinduction bool (blt (trans hds0 i) d) (\lambda (b0: 
-bool).(ex2 C (\lambda (e2: C).(drop1 (match b0 with [true \Rightarrow (PCons 
-h (minus d (S (trans hds0 i))) (ptrans hds0 i)) | false \Rightarrow (ptrans 
-hds0 i)]) e2 e1)) (\lambda (e2: C).(getl (match b0 with [true \Rightarrow 
-(trans hds0 i) | false \Rightarrow (plus (trans hds0 i) h)]) c2 (CHead e2 
-(Bind b) (lift1 (match b0 with [true \Rightarrow (PCons h (minus d (S (trans 
-hds0 i))) (ptrans hds0 i)) | false \Rightarrow (ptrans hds0 i)]) v)))))) 
-(\lambda (x_x: bool).(bool_ind (\lambda (b0: bool).((eq bool (blt (trans hds0 
-i) d) b0) \to (ex2 C (\lambda (e2: C).(drop1 (match b0 with [true \Rightarrow 
-(PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) | false \Rightarrow 
-(ptrans hds0 i)]) e2 e1)) (\lambda (e2: C).(getl (match b0 with [true 
-\Rightarrow (trans hds0 i) | false \Rightarrow (plus (trans hds0 i) h)]) c2 
-(CHead e2 (Bind b) (lift1 (match b0 with [true \Rightarrow (PCons h (minus d 
-(S (trans hds0 i))) (ptrans hds0 i)) | false \Rightarrow (ptrans hds0 i)]) 
-v))))))) (\lambda (H5: (eq bool (blt (trans hds0 i) d) true)).(let H_x0 \def 
-(H c1 x H4 b e1 v i H1) in (let H6 \def H_x0 in (ex2_ind C (\lambda (e2: 
-C).(drop1 (ptrans hds0 i) e2 e1)) (\lambda (e2: C).(getl (trans hds0 i) x 
-(CHead e2 (Bind b) (lift1 (ptrans hds0 i) v)))) (ex2 C (\lambda (e2: 
-C).(drop1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) e2 e1)) 
-(\lambda (e2: C).(getl (trans hds0 i) c2 (CHead e2 (Bind b) (lift1 (PCons h 
-(minus d (S (trans hds0 i))) (ptrans hds0 i)) v))))) (\lambda (x0: 
-C).(\lambda (H7: (drop1 (ptrans hds0 i) x0 e1)).(\lambda (H8: (getl (trans 
-hds0 i) x (CHead x0 (Bind b) (lift1 (ptrans hds0 i) v)))).(let H_x1 \def 
-(drop_getl_trans_lt (trans hds0 i) d (blt_lt d (trans hds0 i) H5) c2 x h H3 b 
-x0 (lift1 (ptrans hds0 i) v) H8) in (let H9 \def H_x1 in (ex2_ind C (\lambda 
-(e2: C).(getl (trans hds0 i) c2 (CHead e2 (Bind b) (lift h (minus d (S (trans 
-hds0 i))) (lift1 (ptrans hds0 i) v))))) (\lambda (e2: C).(drop h (minus d (S 
-(trans hds0 i))) e2 x0)) (ex2 C (\lambda (e2: C).(drop1 (PCons h (minus d (S 
-(trans hds0 i))) (ptrans hds0 i)) e2 e1)) (\lambda (e2: C).(getl (trans hds0 
-i) c2 (CHead e2 (Bind b) (lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans 
-hds0 i)) v))))) (\lambda (x1: C).(\lambda (H10: (getl (trans hds0 i) c2 
-(CHead x1 (Bind b) (lift h (minus d (S (trans hds0 i))) (lift1 (ptrans hds0 
-i) v))))).(\lambda (H11: (drop h (minus d (S (trans hds0 i))) x1 
-x0)).(ex_intro2 C (\lambda (e2: C).(drop1 (PCons h (minus d (S (trans hds0 
-i))) (ptrans hds0 i)) e2 e1)) (\lambda (e2: C).(getl (trans hds0 i) c2 (CHead 
-e2 (Bind b) (lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) 
-v)))) x1 (drop1_cons x1 x0 h (minus d (S (trans hds0 i))) H11 e1 (ptrans hds0 
-i) H7) H10)))) H9)))))) H6)))) (\lambda (H5: (eq bool (blt (trans hds0 i) d) 
-false)).(let H_x0 \def (H c1 x H4 b e1 v i H1) in (let H6 \def H_x0 in 
-(ex2_ind C (\lambda (e2: C).(drop1 (ptrans hds0 i) e2 e1)) (\lambda (e2: 
-C).(getl (trans hds0 i) x (CHead e2 (Bind b) (lift1 (ptrans hds0 i) v)))) 
+(let TMP_2 \def (\lambda (e2: C).(let TMP_1 \def (ptrans p i) in (drop1 TMP_1 
+e2 e1))) in (let TMP_8 \def (\lambda (e2: C).(let TMP_3 \def (trans p i) in 
+(let TMP_4 \def (Bind b) in (let TMP_5 \def (ptrans p i) in (let TMP_6 \def 
+(lift1 TMP_5 v) in (let TMP_7 \def (CHead e2 TMP_4 TMP_6) in (getl TMP_3 c2 
+TMP_7))))))) in (ex2 C TMP_2 TMP_8)))))))))))) in (let TMP_21 \def (\lambda 
+(c1: C).(\lambda (c2: C).(\lambda (H: (drop1 PNil c2 c1)).(\lambda (b: 
+B).(\lambda (e1: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H0: (getl i 
+c1 (CHead e1 (Bind b) v))).(let H_y \def (drop1_gen_pnil c2 c1 H) in (let 
+TMP_14 \def (\lambda (c: C).(let TMP_10 \def (\lambda (e2: C).(drop1 PNil e2 
+e1)) in (let TMP_13 \def (\lambda (e2: C).(let TMP_11 \def (Bind b) in (let 
+TMP_12 \def (CHead e2 TMP_11 v) in (getl i c TMP_12)))) in (ex2 C TMP_10 
+TMP_13)))) in (let TMP_15 \def (\lambda (e2: C).(drop1 PNil e2 e1)) in (let 
+TMP_18 \def (\lambda (e2: C).(let TMP_16 \def (Bind b) in (let TMP_17 \def 
+(CHead e2 TMP_16 v) in (getl i c1 TMP_17)))) in (let TMP_19 \def (drop1_nil 
+e1) in (let TMP_20 \def (ex_intro2 C TMP_15 TMP_18 e1 TMP_19 H0) in (eq_ind_r 
+C c1 TMP_14 TMP_20 c2 H_y))))))))))))))) in (let TMP_210 \def (\lambda (h: 
+nat).(\lambda (d: nat).(\lambda (hds0: PList).(\lambda (H: ((\forall (c1: 
+C).(\forall (c2: C).((drop1 hds0 c2 c1) \to (\forall (b: B).(\forall (e1: 
+C).(\forall (v: T).(\forall (i: nat).((getl i c1 (CHead e1 (Bind b) v)) \to 
 (ex2 C (\lambda (e2: C).(drop1 (ptrans hds0 i) e2 e1)) (\lambda (e2: C).(getl 
-(plus (trans hds0 i) h) c2 (CHead e2 (Bind b) (lift1 (ptrans hds0 i) v))))) 
-(\lambda (x0: C).(\lambda (H7: (drop1 (ptrans hds0 i) x0 e1)).(\lambda (H8: 
-(getl (trans hds0 i) x (CHead x0 (Bind b) (lift1 (ptrans hds0 i) v)))).(let 
-H9 \def (drop_getl_trans_ge (trans hds0 i) c2 x d h H3 (CHead x0 (Bind b) 
-(lift1 (ptrans hds0 i) v)) H8) in (ex_intro2 C (\lambda (e2: C).(drop1 
-(ptrans hds0 i) e2 e1)) (\lambda (e2: C).(getl (plus (trans hds0 i) h) c2 
-(CHead e2 (Bind b) (lift1 (ptrans hds0 i) v)))) x0 H7 (H9 (bge_le d (trans 
-hds0 i) H5))))))) H6)))) x_x)))))) H2))))))))))))))) hds).
-(* COMMENTS
-Initial nodes: 1674
-END *)
+(trans hds0 i) c2 (CHead e2 (Bind b) (lift1 (ptrans hds0 i) 
+v))))))))))))))).(\lambda (c1: C).(\lambda (c2: C).(\lambda (H0: (drop1 
+(PCons h d hds0) c2 c1)).(\lambda (b: B).(\lambda (e1: C).(\lambda (v: 
+T).(\lambda (i: nat).(\lambda (H1: (getl i c1 (CHead e1 (Bind b) v))).(let 
+H_x \def (drop1_gen_pcons c2 c1 hds0 h d H0) in (let H2 \def H_x in (let 
+TMP_22 \def (\lambda (c3: C).(drop h d c2 c3)) in (let TMP_23 \def (\lambda 
+(c3: C).(drop1 hds0 c3 c1)) in (let TMP_31 \def (\lambda (e2: C).(let TMP_24 
+\def (trans hds0 i) in (let TMP_25 \def (blt TMP_24 d) in (let TMP_30 \def 
+(match TMP_25 with [true \Rightarrow (let TMP_26 \def (trans hds0 i) in (let 
+TMP_27 \def (S TMP_26) in (let TMP_28 \def (minus d TMP_27) in (let TMP_29 
+\def (ptrans hds0 i) in (PCons h TMP_28 TMP_29))))) | false \Rightarrow 
+(ptrans hds0 i)]) in (drop1 TMP_30 e2 e1))))) in (let TMP_46 \def (\lambda 
+(e2: C).(let TMP_32 \def (trans hds0 i) in (let TMP_33 \def (blt TMP_32 d) in 
+(let TMP_35 \def (match TMP_33 with [true \Rightarrow (trans hds0 i) | false 
+\Rightarrow (let TMP_34 \def (trans hds0 i) in (plus TMP_34 h))]) in (let 
+TMP_36 \def (Bind b) in (let TMP_37 \def (trans hds0 i) in (let TMP_38 \def 
+(blt TMP_37 d) in (let TMP_43 \def (match TMP_38 with [true \Rightarrow (let 
+TMP_39 \def (trans hds0 i) in (let TMP_40 \def (S TMP_39) in (let TMP_41 \def 
+(minus d TMP_40) in (let TMP_42 \def (ptrans hds0 i) in (PCons h TMP_41 
+TMP_42))))) | false \Rightarrow (ptrans hds0 i)]) in (let TMP_44 \def (lift1 
+TMP_43 v) in (let TMP_45 \def (CHead e2 TMP_36 TMP_44) in (getl TMP_35 c2 
+TMP_45))))))))))) in (let TMP_47 \def (ex2 C TMP_31 TMP_46) in (let TMP_209 
+\def (\lambda (x: C).(\lambda (H3: (drop h d c2 x)).(\lambda (H4: (drop1 hds0 
+x c1)).(let TMP_48 \def (trans hds0 i) in (let TMP_49 \def (blt TMP_48 d) in 
+(let TMP_67 \def (\lambda (b0: bool).(let TMP_55 \def (\lambda (e2: C).(let 
+TMP_54 \def (match b0 with [true \Rightarrow (let TMP_50 \def (trans hds0 i) 
+in (let TMP_51 \def (S TMP_50) in (let TMP_52 \def (minus d TMP_51) in (let 
+TMP_53 \def (ptrans hds0 i) in (PCons h TMP_52 TMP_53))))) | false 
+\Rightarrow (ptrans hds0 i)]) in (drop1 TMP_54 e2 e1))) in (let TMP_66 \def 
+(\lambda (e2: C).(let TMP_57 \def (match b0 with [true \Rightarrow (trans 
+hds0 i) | false \Rightarrow (let TMP_56 \def (trans hds0 i) in (plus TMP_56 
+h))]) in (let TMP_58 \def (Bind b) in (let TMP_63 \def (match b0 with [true 
+\Rightarrow (let TMP_59 \def (trans hds0 i) in (let TMP_60 \def (S TMP_59) in 
+(let TMP_61 \def (minus d TMP_60) in (let TMP_62 \def (ptrans hds0 i) in 
+(PCons h TMP_61 TMP_62))))) | false \Rightarrow (ptrans hds0 i)]) in (let 
+TMP_64 \def (lift1 TMP_63 v) in (let TMP_65 \def (CHead e2 TMP_58 TMP_64) in 
+(getl TMP_57 c2 TMP_65))))))) in (ex2 C TMP_55 TMP_66)))) in (let TMP_208 
+\def (\lambda (x_x: bool).(let TMP_85 \def (\lambda (b0: bool).((eq bool (blt 
+(trans hds0 i) d) b0) \to (let TMP_73 \def (\lambda (e2: C).(let TMP_72 \def 
+(match b0 with [true \Rightarrow (let TMP_68 \def (trans hds0 i) in (let 
+TMP_69 \def (S TMP_68) in (let TMP_70 \def (minus d TMP_69) in (let TMP_71 
+\def (ptrans hds0 i) in (PCons h TMP_70 TMP_71))))) | false \Rightarrow 
+(ptrans hds0 i)]) in (drop1 TMP_72 e2 e1))) in (let TMP_84 \def (\lambda (e2: 
+C).(let TMP_75 \def (match b0 with [true \Rightarrow (trans hds0 i) | false 
+\Rightarrow (let TMP_74 \def (trans hds0 i) in (plus TMP_74 h))]) in (let 
+TMP_76 \def (Bind b) in (let TMP_81 \def (match b0 with [true \Rightarrow 
+(let TMP_77 \def (trans hds0 i) in (let TMP_78 \def (S TMP_77) in (let TMP_79 
+\def (minus d TMP_78) in (let TMP_80 \def (ptrans hds0 i) in (PCons h TMP_79 
+TMP_80))))) | false \Rightarrow (ptrans hds0 i)]) in (let TMP_82 \def (lift1 
+TMP_81 v) in (let TMP_83 \def (CHead e2 TMP_76 TMP_82) in (getl TMP_75 c2 
+TMP_83))))))) in (ex2 C TMP_73 TMP_84))))) in (let TMP_170 \def (\lambda (H5: 
+(eq bool (blt (trans hds0 i) d) true)).(let H_x0 \def (H c1 x H4 b e1 v i H1) 
+in (let H6 \def H_x0 in (let TMP_87 \def (\lambda (e2: C).(let TMP_86 \def 
+(ptrans hds0 i) in (drop1 TMP_86 e2 e1))) in (let TMP_93 \def (\lambda (e2: 
+C).(let TMP_88 \def (trans hds0 i) in (let TMP_89 \def (Bind b) in (let 
+TMP_90 \def (ptrans hds0 i) in (let TMP_91 \def (lift1 TMP_90 v) in (let 
+TMP_92 \def (CHead e2 TMP_89 TMP_91) in (getl TMP_88 x TMP_92))))))) in (let 
+TMP_99 \def (\lambda (e2: C).(let TMP_94 \def (trans hds0 i) in (let TMP_95 
+\def (S TMP_94) in (let TMP_96 \def (minus d TMP_95) in (let TMP_97 \def 
+(ptrans hds0 i) in (let TMP_98 \def (PCons h TMP_96 TMP_97) in (drop1 TMP_98 
+e2 e1))))))) in (let TMP_109 \def (\lambda (e2: C).(let TMP_100 \def (trans 
+hds0 i) in (let TMP_101 \def (Bind b) in (let TMP_102 \def (trans hds0 i) in 
+(let TMP_103 \def (S TMP_102) in (let TMP_104 \def (minus d TMP_103) in (let 
+TMP_105 \def (ptrans hds0 i) in (let TMP_106 \def (PCons h TMP_104 TMP_105) 
+in (let TMP_107 \def (lift1 TMP_106 v) in (let TMP_108 \def (CHead e2 TMP_101 
+TMP_107) in (getl TMP_100 c2 TMP_108))))))))))) in (let TMP_110 \def (ex2 C 
+TMP_99 TMP_109) in (let TMP_169 \def (\lambda (x0: C).(\lambda (H7: (drop1 
+(ptrans hds0 i) x0 e1)).(\lambda (H8: (getl (trans hds0 i) x (CHead x0 (Bind 
+b) (lift1 (ptrans hds0 i) v)))).(let TMP_111 \def (trans hds0 i) in (let 
+TMP_112 \def (trans hds0 i) in (let TMP_113 \def (blt_lt d TMP_112 H5) in 
+(let TMP_114 \def (ptrans hds0 i) in (let TMP_115 \def (lift1 TMP_114 v) in 
+(let H_x1 \def (drop_getl_trans_lt TMP_111 d TMP_113 c2 x h H3 b x0 TMP_115 
+H8) in (let H9 \def H_x1 in (let TMP_125 \def (\lambda (e2: C).(let TMP_116 
+\def (trans hds0 i) in (let TMP_117 \def (Bind b) in (let TMP_118 \def (trans 
+hds0 i) in (let TMP_119 \def (S TMP_118) in (let TMP_120 \def (minus d 
+TMP_119) in (let TMP_121 \def (ptrans hds0 i) in (let TMP_122 \def (lift1 
+TMP_121 v) in (let TMP_123 \def (lift h TMP_120 TMP_122) in (let TMP_124 \def 
+(CHead e2 TMP_117 TMP_123) in (getl TMP_116 c2 TMP_124))))))))))) in (let 
+TMP_129 \def (\lambda (e2: C).(let TMP_126 \def (trans hds0 i) in (let 
+TMP_127 \def (S TMP_126) in (let TMP_128 \def (minus d TMP_127) in (drop h 
+TMP_128 e2 x0))))) in (let TMP_135 \def (\lambda (e2: C).(let TMP_130 \def 
+(trans hds0 i) in (let TMP_131 \def (S TMP_130) in (let TMP_132 \def (minus d 
+TMP_131) in (let TMP_133 \def (ptrans hds0 i) in (let TMP_134 \def (PCons h 
+TMP_132 TMP_133) in (drop1 TMP_134 e2 e1))))))) in (let TMP_145 \def (\lambda 
+(e2: C).(let TMP_136 \def (trans hds0 i) in (let TMP_137 \def (Bind b) in 
+(let TMP_138 \def (trans hds0 i) in (let TMP_139 \def (S TMP_138) in (let 
+TMP_140 \def (minus d TMP_139) in (let TMP_141 \def (ptrans hds0 i) in (let 
+TMP_142 \def (PCons h TMP_140 TMP_141) in (let TMP_143 \def (lift1 TMP_142 v) 
+in (let TMP_144 \def (CHead e2 TMP_137 TMP_143) in (getl TMP_136 c2 
+TMP_144))))))))))) in (let TMP_146 \def (ex2 C TMP_135 TMP_145) in (let 
+TMP_168 \def (\lambda (x1: C).(\lambda (H10: (getl (trans hds0 i) c2 (CHead 
+x1 (Bind b) (lift h (minus d (S (trans hds0 i))) (lift1 (ptrans hds0 i) 
+v))))).(\lambda (H11: (drop h (minus d (S (trans hds0 i))) x1 x0)).(let 
+TMP_152 \def (\lambda (e2: C).(let TMP_147 \def (trans hds0 i) in (let 
+TMP_148 \def (S TMP_147) in (let TMP_149 \def (minus d TMP_148) in (let 
+TMP_150 \def (ptrans hds0 i) in (let TMP_151 \def (PCons h TMP_149 TMP_150) 
+in (drop1 TMP_151 e2 e1))))))) in (let TMP_162 \def (\lambda (e2: C).(let 
+TMP_153 \def (trans hds0 i) in (let TMP_154 \def (Bind b) in (let TMP_155 
+\def (trans hds0 i) in (let TMP_156 \def (S TMP_155) in (let TMP_157 \def 
+(minus d TMP_156) in (let TMP_158 \def (ptrans hds0 i) in (let TMP_159 \def 
+(PCons h TMP_157 TMP_158) in (let TMP_160 \def (lift1 TMP_159 v) in (let 
+TMP_161 \def (CHead e2 TMP_154 TMP_160) in (getl TMP_153 c2 
+TMP_161))))))))))) in (let TMP_163 \def (trans hds0 i) in (let TMP_164 \def 
+(S TMP_163) in (let TMP_165 \def (minus d TMP_164) in (let TMP_166 \def 
+(ptrans hds0 i) in (let TMP_167 \def (drop1_cons x1 x0 h TMP_165 H11 e1 
+TMP_166 H7) in (ex_intro2 C TMP_152 TMP_162 x1 TMP_167 H10))))))))))) in 
+(ex2_ind C TMP_125 TMP_129 TMP_146 TMP_168 H9))))))))))))))))) in (ex2_ind C 
+TMP_87 TMP_93 TMP_110 TMP_169 H6)))))))))) in (let TMP_207 \def (\lambda (H5: 
+(eq bool (blt (trans hds0 i) d) false)).(let H_x0 \def (H c1 x H4 b e1 v i 
+H1) in (let H6 \def H_x0 in (let TMP_172 \def (\lambda (e2: C).(let TMP_171 
+\def (ptrans hds0 i) in (drop1 TMP_171 e2 e1))) in (let TMP_178 \def (\lambda 
+(e2: C).(let TMP_173 \def (trans hds0 i) in (let TMP_174 \def (Bind b) in 
+(let TMP_175 \def (ptrans hds0 i) in (let TMP_176 \def (lift1 TMP_175 v) in 
+(let TMP_177 \def (CHead e2 TMP_174 TMP_176) in (getl TMP_173 x 
+TMP_177))))))) in (let TMP_180 \def (\lambda (e2: C).(let TMP_179 \def 
+(ptrans hds0 i) in (drop1 TMP_179 e2 e1))) in (let TMP_187 \def (\lambda (e2: 
+C).(let TMP_181 \def (trans hds0 i) in (let TMP_182 \def (plus TMP_181 h) in 
+(let TMP_183 \def (Bind b) in (let TMP_184 \def (ptrans hds0 i) in (let 
+TMP_185 \def (lift1 TMP_184 v) in (let TMP_186 \def (CHead e2 TMP_183 
+TMP_185) in (getl TMP_182 c2 TMP_186)))))))) in (let TMP_188 \def (ex2 C 
+TMP_180 TMP_187) in (let TMP_206 \def (\lambda (x0: C).(\lambda (H7: (drop1 
+(ptrans hds0 i) x0 e1)).(\lambda (H8: (getl (trans hds0 i) x (CHead x0 (Bind 
+b) (lift1 (ptrans hds0 i) v)))).(let TMP_189 \def (trans hds0 i) in (let 
+TMP_190 \def (Bind b) in (let TMP_191 \def (ptrans hds0 i) in (let TMP_192 
+\def (lift1 TMP_191 v) in (let TMP_193 \def (CHead x0 TMP_190 TMP_192) in 
+(let H9 \def (drop_getl_trans_ge TMP_189 c2 x d h H3 TMP_193 H8) in (let 
+TMP_195 \def (\lambda (e2: C).(let TMP_194 \def (ptrans hds0 i) in (drop1 
+TMP_194 e2 e1))) in (let TMP_202 \def (\lambda (e2: C).(let TMP_196 \def 
+(trans hds0 i) in (let TMP_197 \def (plus TMP_196 h) in (let TMP_198 \def 
+(Bind b) in (let TMP_199 \def (ptrans hds0 i) in (let TMP_200 \def (lift1 
+TMP_199 v) in (let TMP_201 \def (CHead e2 TMP_198 TMP_200) in (getl TMP_197 
+c2 TMP_201)))))))) in (let TMP_203 \def (trans hds0 i) in (let TMP_204 \def 
+(bge_le d TMP_203 H5) in (let TMP_205 \def (H9 TMP_204) in (ex_intro2 C 
+TMP_195 TMP_202 x0 H7 TMP_205))))))))))))))) in (ex2_ind C TMP_172 TMP_178 
+TMP_188 TMP_206 H6)))))))))) in (bool_ind TMP_85 TMP_170 TMP_207 x_x))))) in 
+(xinduction bool TMP_49 TMP_67 TMP_208)))))))) in (ex2_ind C TMP_22 TMP_23 
+TMP_47 TMP_209 H2))))))))))))))))))))) in (PList_ind TMP_9 TMP_21 TMP_210 
+hds)))).
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/drop1/props.ma b/matita/matita/contribs/lambdadelta/basic_1/drop1/props.ma
index 240219b9589db7e9ab36fe1920aacc11a420c3ff..bab26365fa7dcb6e2186cae2c845d0f500589d8b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/drop1/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/drop1/props.ma
@@ -14,37 +14,50 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/drop1/fwd.ma".
+include "basic_1/drop1/fwd.ma".
 
-include "Basic-1/drop/props.ma".
+include "basic_1/drop/props.ma".
 
-include "Basic-1/getl/defs.ma".
+include "basic_1/getl/defs.ma".
 
 theorem drop1_skip_bind:
  \forall (b: B).(\forall (e: C).(\forall (hds: PList).(\forall (c: 
 C).(\forall (u: T).((drop1 hds c e) \to (drop1 (Ss hds) (CHead c (Bind b) 
 (lift1 hds u)) (CHead e (Bind b) u)))))))
 \def
- \lambda (b: B).(\lambda (e: C).(\lambda (hds: PList).(PList_ind (\lambda (p: 
-PList).(\forall (c: C).(\forall (u: T).((drop1 p c e) \to (drop1 (Ss p) 
-(CHead c (Bind b) (lift1 p u)) (CHead e (Bind b) u)))))) (\lambda (c: 
-C).(\lambda (u: T).(\lambda (H: (drop1 PNil c e)).(let H_y \def 
-(drop1_gen_pnil c e H) in (eq_ind_r C e (\lambda (c0: C).(drop1 PNil (CHead 
-c0 (Bind b) u) (CHead e (Bind b) u))) (drop1_nil (CHead e (Bind b) u)) c 
-H_y))))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda 
-(H: ((\forall (c: C).(\forall (u: T).((drop1 p c e) \to (drop1 (Ss p) (CHead 
-c (Bind b) (lift1 p u)) (CHead e (Bind b) u))))))).(\lambda (c: C).(\lambda 
-(u: T).(\lambda (H0: (drop1 (PCons n n0 p) c e)).(let H_x \def 
-(drop1_gen_pcons c e p n n0 H0) in (let H1 \def H_x in (ex2_ind C (\lambda 
-(c2: C).(drop n n0 c c2)) (\lambda (c2: C).(drop1 p c2 e)) (drop1 (PCons n (S 
-n0) (Ss p)) (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead e (Bind b) u)) 
-(\lambda (x: C).(\lambda (H2: (drop n n0 c x)).(\lambda (H3: (drop1 p x 
-e)).(drop1_cons (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead x (Bind b) 
-(lift1 p u)) n (S n0) (drop_skip_bind n n0 c x H2 b (lift1 p u)) (CHead e 
-(Bind b) u) (Ss p) (H x u H3))))) H1)))))))))) hds))).
-(* COMMENTS
-Initial nodes: 379
-END *)
+ \lambda (b: B).(\lambda (e: C).(\lambda (hds: PList).(let TMP_7 \def 
+(\lambda (p: PList).(\forall (c: C).(\forall (u: T).((drop1 p c e) \to (let 
+TMP_1 \def (Ss p) in (let TMP_2 \def (Bind b) in (let TMP_3 \def (lift1 p u) 
+in (let TMP_4 \def (CHead c TMP_2 TMP_3) in (let TMP_5 \def (Bind b) in (let 
+TMP_6 \def (CHead e TMP_5 u) in (drop1 TMP_1 TMP_4 TMP_6))))))))))) in (let 
+TMP_16 \def (\lambda (c: C).(\lambda (u: T).(\lambda (H: (drop1 PNil c 
+e)).(let H_y \def (drop1_gen_pnil c e H) in (let TMP_12 \def (\lambda (c0: 
+C).(let TMP_8 \def (Bind b) in (let TMP_9 \def (CHead c0 TMP_8 u) in (let 
+TMP_10 \def (Bind b) in (let TMP_11 \def (CHead e TMP_10 u) in (drop1 PNil 
+TMP_9 TMP_11)))))) in (let TMP_13 \def (Bind b) in (let TMP_14 \def (CHead e 
+TMP_13 u) in (let TMP_15 \def (drop1_nil TMP_14) in (eq_ind_r C e TMP_12 
+TMP_15 c H_y))))))))) in (let TMP_44 \def (\lambda (n: nat).(\lambda (n0: 
+nat).(\lambda (p: PList).(\lambda (H: ((\forall (c: C).(\forall (u: 
+T).((drop1 p c e) \to (drop1 (Ss p) (CHead c (Bind b) (lift1 p u)) (CHead e 
+(Bind b) u))))))).(\lambda (c: C).(\lambda (u: T).(\lambda (H0: (drop1 (PCons 
+n n0 p) c e)).(let H_x \def (drop1_gen_pcons c e p n n0 H0) in (let H1 \def 
+H_x in (let TMP_17 \def (\lambda (c2: C).(drop n n0 c c2)) in (let TMP_18 
+\def (\lambda (c2: C).(drop1 p c2 e)) in (let TMP_19 \def (S n0) in (let 
+TMP_20 \def (Ss p) in (let TMP_21 \def (PCons n TMP_19 TMP_20) in (let TMP_22 
+\def (Bind b) in (let TMP_23 \def (lift1 p u) in (let TMP_24 \def (lift n n0 
+TMP_23) in (let TMP_25 \def (CHead c TMP_22 TMP_24) in (let TMP_26 \def (Bind 
+b) in (let TMP_27 \def (CHead e TMP_26 u) in (let TMP_28 \def (drop1 TMP_21 
+TMP_25 TMP_27) in (let TMP_43 \def (\lambda (x: C).(\lambda (H2: (drop n n0 c 
+x)).(\lambda (H3: (drop1 p x e)).(let TMP_29 \def (Bind b) in (let TMP_30 
+\def (lift1 p u) in (let TMP_31 \def (lift n n0 TMP_30) in (let TMP_32 \def 
+(CHead c TMP_29 TMP_31) in (let TMP_33 \def (Bind b) in (let TMP_34 \def 
+(lift1 p u) in (let TMP_35 \def (CHead x TMP_33 TMP_34) in (let TMP_36 \def 
+(S n0) in (let TMP_37 \def (lift1 p u) in (let TMP_38 \def (drop_skip_bind n 
+n0 c x H2 b TMP_37) in (let TMP_39 \def (Bind b) in (let TMP_40 \def (CHead e 
+TMP_39 u) in (let TMP_41 \def (Ss p) in (let TMP_42 \def (H x u H3) in 
+(drop1_cons TMP_32 TMP_35 n TMP_36 TMP_38 TMP_40 TMP_41 
+TMP_42)))))))))))))))))) in (ex2_ind C TMP_17 TMP_18 TMP_28 TMP_43 
+H1))))))))))))))))))))))) in (PList_ind TMP_7 TMP_16 TMP_44 hds)))))).
 
 theorem drop1_cons_tail:
  \forall (c2: C).(\forall (c3: C).(\forall (h: nat).(\forall (d: nat).((drop 
@@ -52,46 +65,50 @@ h d c2 c3) \to (\forall (hds: PList).(\forall (c1: C).((drop1 hds c1 c2) \to
 (drop1 (PConsTail hds h d) c1 c3))))))))
 \def
  \lambda (c2: C).(\lambda (c3: C).(\lambda (h: nat).(\lambda (d: 
-nat).(\lambda (H: (drop h d c2 c3)).(\lambda (hds: PList).(PList_ind (\lambda 
-(p: PList).(\forall (c1: C).((drop1 p c1 c2) \to (drop1 (PConsTail p h d) c1 
-c3)))) (\lambda (c1: C).(\lambda (H0: (drop1 PNil c1 c2)).(let H_y \def 
-(drop1_gen_pnil c1 c2 H0) in (eq_ind_r C c2 (\lambda (c: C).(drop1 (PCons h d 
-PNil) c c3)) (drop1_cons c2 c3 h d H c3 PNil (drop1_nil c3)) c1 H_y)))) 
-(\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H0: 
-((\forall (c1: C).((drop1 p c1 c2) \to (drop1 (PConsTail p h d) c1 
-c3))))).(\lambda (c1: C).(\lambda (H1: (drop1 (PCons n n0 p) c1 c2)).(let H_x 
-\def (drop1_gen_pcons c1 c2 p n n0 H1) in (let H2 \def H_x in (ex2_ind C 
-(\lambda (c4: C).(drop n n0 c1 c4)) (\lambda (c4: C).(drop1 p c4 c2)) (drop1 
-(PCons n n0 (PConsTail p h d)) c1 c3) (\lambda (x: C).(\lambda (H3: (drop n 
-n0 c1 x)).(\lambda (H4: (drop1 p x c2)).(drop1_cons c1 x n n0 H3 c3 
-(PConsTail p h d) (H0 x H4))))) H2))))))))) hds)))))).
-(* COMMENTS
-Initial nodes: 271
-END *)
+nat).(\lambda (H: (drop h d c2 c3)).(\lambda (hds: PList).(let TMP_2 \def 
+(\lambda (p: PList).(\forall (c1: C).((drop1 p c1 c2) \to (let TMP_1 \def 
+(PConsTail p h d) in (drop1 TMP_1 c1 c3))))) in (let TMP_7 \def (\lambda (c1: 
+C).(\lambda (H0: (drop1 PNil c1 c2)).(let H_y \def (drop1_gen_pnil c1 c2 H0) 
+in (let TMP_4 \def (\lambda (c: C).(let TMP_3 \def (PCons h d PNil) in (drop1 
+TMP_3 c c3))) in (let TMP_5 \def (drop1_nil c3) in (let TMP_6 \def 
+(drop1_cons c2 c3 h d H c3 PNil TMP_5) in (eq_ind_r C c2 TMP_4 TMP_6 c1 
+H_y))))))) in (let TMP_16 \def (\lambda (n: nat).(\lambda (n0: nat).(\lambda 
+(p: PList).(\lambda (H0: ((\forall (c1: C).((drop1 p c1 c2) \to (drop1 
+(PConsTail p h d) c1 c3))))).(\lambda (c1: C).(\lambda (H1: (drop1 (PCons n 
+n0 p) c1 c2)).(let H_x \def (drop1_gen_pcons c1 c2 p n n0 H1) in (let H2 \def 
+H_x in (let TMP_8 \def (\lambda (c4: C).(drop n n0 c1 c4)) in (let TMP_9 \def 
+(\lambda (c4: C).(drop1 p c4 c2)) in (let TMP_10 \def (PConsTail p h d) in 
+(let TMP_11 \def (PCons n n0 TMP_10) in (let TMP_12 \def (drop1 TMP_11 c1 c3) 
+in (let TMP_15 \def (\lambda (x: C).(\lambda (H3: (drop n n0 c1 x)).(\lambda 
+(H4: (drop1 p x c2)).(let TMP_13 \def (PConsTail p h d) in (let TMP_14 \def 
+(H0 x H4) in (drop1_cons c1 x n n0 H3 c3 TMP_13 TMP_14)))))) in (ex2_ind C 
+TMP_8 TMP_9 TMP_12 TMP_15 H2))))))))))))))) in (PList_ind TMP_2 TMP_7 TMP_16 
+hds))))))))).
 
 theorem drop1_trans:
  \forall (is1: PList).(\forall (c1: C).(\forall (c0: C).((drop1 is1 c1 c0) 
 \to (\forall (is2: PList).(\forall (c2: C).((drop1 is2 c0 c2) \to (drop1 
 (papp is1 is2) c1 c2)))))))
 \def
- \lambda (is1: PList).(PList_ind (\lambda (p: PList).(\forall (c1: 
+ \lambda (is1: PList).(let TMP_2 \def (\lambda (p: PList).(\forall (c1: 
 C).(\forall (c0: C).((drop1 p c1 c0) \to (\forall (is2: PList).(\forall (c2: 
-C).((drop1 is2 c0 c2) \to (drop1 (papp p is2) c1 c2)))))))) (\lambda (c1: 
-C).(\lambda (c0: C).(\lambda (H: (drop1 PNil c1 c0)).(\lambda (is2: 
-PList).(\lambda (c2: C).(\lambda (H0: (drop1 is2 c0 c2)).(let H_y \def 
-(drop1_gen_pnil c1 c0 H) in (let H1 \def (eq_ind_r C c0 (\lambda (c: 
-C).(drop1 is2 c c2)) H0 c1 H_y) in H1)))))))) (\lambda (n: nat).(\lambda (n0: 
+C).((drop1 is2 c0 c2) \to (let TMP_1 \def (papp p is2) in (drop1 TMP_1 c1 
+c2))))))))) in (let TMP_4 \def (\lambda (c1: C).(\lambda (c0: C).(\lambda (H: 
+(drop1 PNil c1 c0)).(\lambda (is2: PList).(\lambda (c2: C).(\lambda (H0: 
+(drop1 is2 c0 c2)).(let H_y \def (drop1_gen_pnil c1 c0 H) in (let TMP_3 \def 
+(\lambda (c: C).(drop1 is2 c c2)) in (let H1 \def (eq_ind_r C c0 TMP_3 H0 c1 
+H_y) in H1))))))))) in (let TMP_13 \def (\lambda (n: nat).(\lambda (n0: 
 nat).(\lambda (p: PList).(\lambda (H: ((\forall (c1: C).(\forall (c0: 
 C).((drop1 p c1 c0) \to (\forall (is2: PList).(\forall (c2: C).((drop1 is2 c0 
 c2) \to (drop1 (papp p is2) c1 c2))))))))).(\lambda (c1: C).(\lambda (c0: 
 C).(\lambda (H0: (drop1 (PCons n n0 p) c1 c0)).(\lambda (is2: PList).(\lambda 
 (c2: C).(\lambda (H1: (drop1 is2 c0 c2)).(let H_x \def (drop1_gen_pcons c1 c0 
-p n n0 H0) in (let H2 \def H_x in (ex2_ind C (\lambda (c3: C).(drop n n0 c1 
-c3)) (\lambda (c3: C).(drop1 p c3 c0)) (drop1 (PCons n n0 (papp p is2)) c1 
-c2) (\lambda (x: C).(\lambda (H3: (drop n n0 c1 x)).(\lambda (H4: (drop1 p x 
-c0)).(drop1_cons c1 x n n0 H3 c2 (papp p is2) (H x c0 H4 is2 c2 H1))))) 
-H2))))))))))))) is1).
-(* COMMENTS
-Initial nodes: 287
-END *)
+p n n0 H0) in (let H2 \def H_x in (let TMP_5 \def (\lambda (c3: C).(drop n n0 
+c1 c3)) in (let TMP_6 \def (\lambda (c3: C).(drop1 p c3 c0)) in (let TMP_7 
+\def (papp p is2) in (let TMP_8 \def (PCons n n0 TMP_7) in (let TMP_9 \def 
+(drop1 TMP_8 c1 c2) in (let TMP_12 \def (\lambda (x: C).(\lambda (H3: (drop n 
+n0 c1 x)).(\lambda (H4: (drop1 p x c0)).(let TMP_10 \def (papp p is2) in (let 
+TMP_11 \def (H x c0 H4 is2 c2 H1) in (drop1_cons c1 x n n0 H3 c2 TMP_10 
+TMP_11)))))) in (ex2_ind C TMP_5 TMP_6 TMP_9 TMP_12 H2))))))))))))))))))) in 
+(PList_ind TMP_2 TMP_4 TMP_13 is1)))).
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/lift1/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/lift1/defs.ma
index 1f473cbcecdfc54b967797bd30a0a2c10804cb5a..1e1080c89c842dc0d31a89c99e3039c3788d3b34 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/lift1/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/lift1/defs.ma
@@ -14,27 +14,18 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/lift/defs.ma".
+include "basic_1/lift/defs.ma".
 
-definition trans:
- PList \to (nat \to nat)
-\def
- let rec trans (hds: PList) on hds: (nat \to nat) \def (\lambda (i: 
-nat).(match hds with [PNil \Rightarrow i | (PCons h d hds0) \Rightarrow (let 
-j \def (trans hds0 i) in (match (blt j d) with [true \Rightarrow j | false 
-\Rightarrow (plus j h)]))])) in trans.
+let rec trans (hds: PList) on hds: nat \to nat \def \lambda (i: nat).(match 
+hds with [PNil \Rightarrow i | (PCons h d hds0) \Rightarrow (let j \def 
+(trans hds0 i) in (let TMP_1 \def (blt j d) in (match TMP_1 with [true 
+\Rightarrow j | false \Rightarrow (plus j h)])))]).
 
-definition lift1:
- PList \to (T \to T)
-\def
- let rec lift1 (hds: PList) on hds: (T \to T) \def (\lambda (t: T).(match hds 
-with [PNil \Rightarrow t | (PCons h d hds0) \Rightarrow (lift h d (lift1 hds0 
-t))])) in lift1.
+let rec lift1 (hds: PList) on hds: T \to T \def \lambda (t: T).(match hds 
+with [PNil \Rightarrow t | (PCons h d hds0) \Rightarrow (let TMP_1 \def 
+(lift1 hds0 t) in (lift h d TMP_1))]).
 
-definition lifts1:
- PList \to (TList \to TList)
-\def
- let rec lifts1 (hds: PList) (ts: TList) on ts: TList \def (match ts with 
-[TNil \Rightarrow TNil | (TCons t ts0) \Rightarrow (TCons (lift1 hds t) 
-(lifts1 hds ts0))]) in lifts1.
+let rec lifts1 (hds: PList) (ts: TList) on ts: TList \def match ts with [TNil 
+\Rightarrow TNil | (TCons t ts0) \Rightarrow (let TMP_1 \def (lift1 hds t) in 
+(let TMP_2 \def (lifts1 hds ts0) in (TCons TMP_1 TMP_2)))].
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/lift1/drop1.ma b/matita/matita/contribs/lambdadelta/basic_1/lift1/drop1.ma
new file mode 100644 (file)
index 0000000..459fcb8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_1/lift1/drop1.ma
@@ -0,0 +1,281 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "basic_1/lift/props.ma".
+
+include "basic_1/drop1/defs.ma".
+
+theorem lift1_lift1:
+ \forall (is1: PList).(\forall (is2: PList).(\forall (t: T).(eq T (lift1 is1 
+(lift1 is2 t)) (lift1 (papp is1 is2) t))))
+\def
+ \lambda (is1: PList).(let TMP_5 \def (\lambda (p: PList).(\forall (is2: 
+PList).(\forall (t: T).(let TMP_1 \def (lift1 is2 t) in (let TMP_2 \def 
+(lift1 p TMP_1) in (let TMP_3 \def (papp p is2) in (let TMP_4 \def (lift1 
+TMP_3 t) in (eq T TMP_2 TMP_4)))))))) in (let TMP_7 \def (\lambda (is2: 
+PList).(\lambda (t: T).(let TMP_6 \def (lift1 is2 t) in (refl_equal T 
+TMP_6)))) in (let TMP_15 \def (\lambda (n: nat).(\lambda (n0: nat).(\lambda 
+(p: PList).(\lambda (H: ((\forall (is2: PList).(\forall (t: T).(eq T (lift1 p 
+(lift1 is2 t)) (lift1 (papp p is2) t)))))).(\lambda (is2: PList).(\lambda (t: 
+T).(let TMP_8 \def (lift1 is2 t) in (let TMP_9 \def (lift1 p TMP_8) in (let 
+TMP_10 \def (papp p is2) in (let TMP_11 \def (lift1 TMP_10 t) in (let TMP_12 
+\def (refl_equal nat n) in (let TMP_13 \def (refl_equal nat n0) in (let 
+TMP_14 \def (H is2 t) in (f_equal3 nat nat T T lift n n n0 n0 TMP_9 TMP_11 
+TMP_12 TMP_13 TMP_14)))))))))))))) in (PList_ind TMP_5 TMP_7 TMP_15 is1)))).
+
+theorem lift1_xhg:
+ \forall (hds: PList).(\forall (t: T).(eq T (lift1 (Ss hds) (lift (S O) O t)) 
+(lift (S O) O (lift1 hds t))))
+\def
+ \lambda (hds: PList).(let TMP_8 \def (\lambda (p: PList).(\forall (t: 
+T).(let TMP_1 \def (Ss p) in (let TMP_2 \def (S O) in (let TMP_3 \def (lift 
+TMP_2 O t) in (let TMP_4 \def (lift1 TMP_1 TMP_3) in (let TMP_5 \def (S O) in 
+(let TMP_6 \def (lift1 p t) in (let TMP_7 \def (lift TMP_5 O TMP_6) in (eq T 
+TMP_4 TMP_7)))))))))) in (let TMP_11 \def (\lambda (t: T).(let TMP_9 \def (S 
+O) in (let TMP_10 \def (lift TMP_9 O t) in (refl_equal T TMP_10)))) in (let 
+TMP_67 \def (\lambda (h: nat).(\lambda (d: nat).(\lambda (p: PList).(\lambda 
+(H: ((\forall (t: T).(eq T (lift1 (Ss p) (lift (S O) O t)) (lift (S O) O 
+(lift1 p t)))))).(\lambda (t: T).(let TMP_12 \def (S O) in (let TMP_13 \def 
+(lift1 p t) in (let TMP_14 \def (lift TMP_12 O TMP_13) in (let TMP_21 \def 
+(\lambda (t0: T).(let TMP_15 \def (S d) in (let TMP_16 \def (lift h TMP_15 
+t0) in (let TMP_17 \def (S O) in (let TMP_18 \def (lift1 p t) in (let TMP_19 
+\def (lift h d TMP_18) in (let TMP_20 \def (lift TMP_17 O TMP_19) in (eq T 
+TMP_16 TMP_20)))))))) in (let TMP_22 \def (S O) in (let TMP_23 \def (plus 
+TMP_22 d) in (let TMP_32 \def (\lambda (n: nat).(let TMP_24 \def (S O) in 
+(let TMP_25 \def (lift1 p t) in (let TMP_26 \def (lift TMP_24 O TMP_25) in 
+(let TMP_27 \def (lift h n TMP_26) in (let TMP_28 \def (S O) in (let TMP_29 
+\def (lift1 p t) in (let TMP_30 \def (lift h d TMP_29) in (let TMP_31 \def 
+(lift TMP_28 O TMP_30) in (eq T TMP_27 TMP_31)))))))))) in (let TMP_33 \def 
+(S O) in (let TMP_34 \def (lift1 p t) in (let TMP_35 \def (lift h d TMP_34) 
+in (let TMP_36 \def (lift TMP_33 O TMP_35) in (let TMP_41 \def (\lambda (t0: 
+T).(let TMP_37 \def (S O) in (let TMP_38 \def (lift1 p t) in (let TMP_39 \def 
+(lift h d TMP_38) in (let TMP_40 \def (lift TMP_37 O TMP_39) in (eq T t0 
+TMP_40)))))) in (let TMP_42 \def (S O) in (let TMP_43 \def (lift1 p t) in 
+(let TMP_44 \def (lift h d TMP_43) in (let TMP_45 \def (lift TMP_42 O TMP_44) 
+in (let TMP_46 \def (refl_equal T TMP_45) in (let TMP_47 \def (S O) in (let 
+TMP_48 \def (plus TMP_47 d) in (let TMP_49 \def (S O) in (let TMP_50 \def 
+(lift1 p t) in (let TMP_51 \def (lift TMP_49 O TMP_50) in (let TMP_52 \def 
+(lift h TMP_48 TMP_51) in (let TMP_53 \def (lift1 p t) in (let TMP_54 \def (S 
+O) in (let TMP_55 \def (le_O_n d) in (let TMP_56 \def (lift_d TMP_53 h TMP_54 
+d O TMP_55) in (let TMP_57 \def (eq_ind_r T TMP_36 TMP_41 TMP_46 TMP_52 
+TMP_56) in (let TMP_58 \def (S d) in (let TMP_59 \def (S d) in (let TMP_60 
+\def (refl_equal nat TMP_59) in (let TMP_61 \def (eq_ind nat TMP_23 TMP_32 
+TMP_57 TMP_58 TMP_60) in (let TMP_62 \def (Ss p) in (let TMP_63 \def (S O) in 
+(let TMP_64 \def (lift TMP_63 O t) in (let TMP_65 \def (lift1 TMP_62 TMP_64) 
+in (let TMP_66 \def (H t) in (eq_ind_r T TMP_14 TMP_21 TMP_61 TMP_65 
+TMP_66))))))))))))))))))))))))))))))))))))))))))) in (PList_ind TMP_8 TMP_11 
+TMP_67 hds)))).
+
+theorem lifts1_xhg:
+ \forall (hds: PList).(\forall (ts: TList).(eq TList (lifts1 (Ss hds) (lifts 
+(S O) O ts)) (lifts (S O) O (lifts1 hds ts))))
+\def
+ \lambda (hds: PList).(\lambda (ts: TList).(let TMP_8 \def (\lambda (t: 
+TList).(let TMP_1 \def (Ss hds) in (let TMP_2 \def (S O) in (let TMP_3 \def 
+(lifts TMP_2 O t) in (let TMP_4 \def (lifts1 TMP_1 TMP_3) in (let TMP_5 \def 
+(S O) in (let TMP_6 \def (lifts1 hds t) in (let TMP_7 \def (lifts TMP_5 O 
+TMP_6) in (eq TList TMP_4 TMP_7))))))))) in (let TMP_9 \def (refl_equal TList 
+TNil) in (let TMP_59 \def (\lambda (t: T).(\lambda (t0: TList).(\lambda (H: 
+(eq TList (lifts1 (Ss hds) (lifts (S O) O t0)) (lifts (S O) O (lifts1 hds 
+t0)))).(let TMP_10 \def (S O) in (let TMP_11 \def (lift1 hds t) in (let 
+TMP_12 \def (lift TMP_10 O TMP_11) in (let TMP_25 \def (\lambda (t1: T).(let 
+TMP_13 \def (Ss hds) in (let TMP_14 \def (S O) in (let TMP_15 \def (lifts 
+TMP_14 O t0) in (let TMP_16 \def (lifts1 TMP_13 TMP_15) in (let TMP_17 \def 
+(TCons t1 TMP_16) in (let TMP_18 \def (S O) in (let TMP_19 \def (lift1 hds t) 
+in (let TMP_20 \def (lift TMP_18 O TMP_19) in (let TMP_21 \def (S O) in (let 
+TMP_22 \def (lifts1 hds t0) in (let TMP_23 \def (lifts TMP_21 O TMP_22) in 
+(let TMP_24 \def (TCons TMP_20 TMP_23) in (eq TList TMP_17 
+TMP_24)))))))))))))) in (let TMP_26 \def (S O) in (let TMP_27 \def (lifts1 
+hds t0) in (let TMP_28 \def (lifts TMP_26 O TMP_27) in (let TMP_40 \def 
+(\lambda (t1: TList).(let TMP_29 \def (S O) in (let TMP_30 \def (lift1 hds t) 
+in (let TMP_31 \def (lift TMP_29 O TMP_30) in (let TMP_32 \def (TCons TMP_31 
+t1) in (let TMP_33 \def (S O) in (let TMP_34 \def (lift1 hds t) in (let 
+TMP_35 \def (lift TMP_33 O TMP_34) in (let TMP_36 \def (S O) in (let TMP_37 
+\def (lifts1 hds t0) in (let TMP_38 \def (lifts TMP_36 O TMP_37) in (let 
+TMP_39 \def (TCons TMP_35 TMP_38) in (eq TList TMP_32 TMP_39))))))))))))) in 
+(let TMP_41 \def (S O) in (let TMP_42 \def (lift1 hds t) in (let TMP_43 \def 
+(lift TMP_41 O TMP_42) in (let TMP_44 \def (S O) in (let TMP_45 \def (lifts1 
+hds t0) in (let TMP_46 \def (lifts TMP_44 O TMP_45) in (let TMP_47 \def 
+(TCons TMP_43 TMP_46) in (let TMP_48 \def (refl_equal TList TMP_47) in (let 
+TMP_49 \def (Ss hds) in (let TMP_50 \def (S O) in (let TMP_51 \def (lifts 
+TMP_50 O t0) in (let TMP_52 \def (lifts1 TMP_49 TMP_51) in (let TMP_53 \def 
+(eq_ind_r TList TMP_28 TMP_40 TMP_48 TMP_52 H) in (let TMP_54 \def (Ss hds) 
+in (let TMP_55 \def (S O) in (let TMP_56 \def (lift TMP_55 O t) in (let 
+TMP_57 \def (lift1 TMP_54 TMP_56) in (let TMP_58 \def (lift1_xhg hds t) in 
+(eq_ind_r T TMP_12 TMP_25 TMP_53 TMP_57 TMP_58)))))))))))))))))))))))))))))) 
+in (TList_ind TMP_8 TMP_9 TMP_59 ts))))).
+
+theorem lift1_free:
+ \forall (hds: PList).(\forall (i: nat).(\forall (t: T).(eq T (lift1 hds 
+(lift (S i) O t)) (lift (S (trans hds i)) O (lift1 (ptrans hds i) t)))))
+\def
+ \lambda (hds: PList).(let TMP_9 \def (\lambda (p: PList).(\forall (i: 
+nat).(\forall (t: T).(let TMP_1 \def (S i) in (let TMP_2 \def (lift TMP_1 O 
+t) in (let TMP_3 \def (lift1 p TMP_2) in (let TMP_4 \def (trans p i) in (let 
+TMP_5 \def (S TMP_4) in (let TMP_6 \def (ptrans p i) in (let TMP_7 \def 
+(lift1 TMP_6 t) in (let TMP_8 \def (lift TMP_5 O TMP_7) in (eq T TMP_3 
+TMP_8)))))))))))) in (let TMP_12 \def (\lambda (i: nat).(\lambda (t: T).(let 
+TMP_10 \def (S i) in (let TMP_11 \def (lift TMP_10 O t) in (refl_equal T 
+TMP_11))))) in (let TMP_262 \def (\lambda (h: nat).(\lambda (d: nat).(\lambda 
+(hds0: PList).(\lambda (H: ((\forall (i: nat).(\forall (t: T).(eq T (lift1 
+hds0 (lift (S i) O t)) (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) 
+t))))))).(\lambda (i: nat).(\lambda (t: T).(let TMP_13 \def (trans hds0 i) in 
+(let TMP_14 \def (S TMP_13) in (let TMP_15 \def (ptrans hds0 i) in (let 
+TMP_16 \def (lift1 TMP_15 t) in (let TMP_17 \def (lift TMP_14 O TMP_16) in 
+(let TMP_33 \def (\lambda (t0: T).(let TMP_18 \def (lift h d t0) in (let 
+TMP_19 \def (trans hds0 i) in (let TMP_20 \def (blt TMP_19 d) in (let TMP_22 
+\def (match TMP_20 with [true \Rightarrow (trans hds0 i) | false \Rightarrow 
+(let TMP_21 \def (trans hds0 i) in (plus TMP_21 h))]) in (let TMP_23 \def (S 
+TMP_22) in (let TMP_24 \def (trans hds0 i) in (let TMP_25 \def (blt TMP_24 d) 
+in (let TMP_30 \def (match TMP_25 with [true \Rightarrow (let TMP_26 \def 
+(trans hds0 i) in (let TMP_27 \def (S TMP_26) in (let TMP_28 \def (minus d 
+TMP_27) in (let TMP_29 \def (ptrans hds0 i) in (PCons h TMP_28 TMP_29))))) | 
+false \Rightarrow (ptrans hds0 i)]) in (let TMP_31 \def (lift1 TMP_30 t) in 
+(let TMP_32 \def (lift TMP_23 O TMP_31) in (eq T TMP_18 TMP_32)))))))))))) in 
+(let TMP_34 \def (trans hds0 i) in (let TMP_35 \def (blt TMP_34 d) in (let 
+TMP_52 \def (\lambda (b: bool).(let TMP_36 \def (trans hds0 i) in (let TMP_37 
+\def (S TMP_36) in (let TMP_38 \def (ptrans hds0 i) in (let TMP_39 \def 
+(lift1 TMP_38 t) in (let TMP_40 \def (lift TMP_37 O TMP_39) in (let TMP_41 
+\def (lift h d TMP_40) in (let TMP_43 \def (match b with [true \Rightarrow 
+(trans hds0 i) | false \Rightarrow (let TMP_42 \def (trans hds0 i) in (plus 
+TMP_42 h))]) in (let TMP_44 \def (S TMP_43) in (let TMP_49 \def (match b with 
+[true \Rightarrow (let TMP_45 \def (trans hds0 i) in (let TMP_46 \def (S 
+TMP_45) in (let TMP_47 \def (minus d TMP_46) in (let TMP_48 \def (ptrans hds0 
+i) in (PCons h TMP_47 TMP_48))))) | false \Rightarrow (ptrans hds0 i)]) in 
+(let TMP_50 \def (lift1 TMP_49 t) in (let TMP_51 \def (lift TMP_44 O TMP_50) 
+in (eq T TMP_41 TMP_51))))))))))))) in (let TMP_256 \def (\lambda (x_x: 
+bool).(let TMP_69 \def (\lambda (b: bool).((eq bool (blt (trans hds0 i) d) b) 
+\to (let TMP_53 \def (trans hds0 i) in (let TMP_54 \def (S TMP_53) in (let 
+TMP_55 \def (ptrans hds0 i) in (let TMP_56 \def (lift1 TMP_55 t) in (let 
+TMP_57 \def (lift TMP_54 O TMP_56) in (let TMP_58 \def (lift h d TMP_57) in 
+(let TMP_60 \def (match b with [true \Rightarrow (trans hds0 i) | false 
+\Rightarrow (let TMP_59 \def (trans hds0 i) in (plus TMP_59 h))]) in (let 
+TMP_61 \def (S TMP_60) in (let TMP_66 \def (match b with [true \Rightarrow 
+(let TMP_62 \def (trans hds0 i) in (let TMP_63 \def (S TMP_62) in (let TMP_64 
+\def (minus d TMP_63) in (let TMP_65 \def (ptrans hds0 i) in (PCons h TMP_64 
+TMP_65))))) | false \Rightarrow (ptrans hds0 i)]) in (let TMP_67 \def (lift1 
+TMP_66 t) in (let TMP_68 \def (lift TMP_61 O TMP_67) in (eq T TMP_58 
+TMP_68)))))))))))))) in (let TMP_159 \def (\lambda (H0: (eq bool (blt (trans 
+hds0 i) d) true)).(let TMP_70 \def (trans hds0 i) in (let TMP_71 \def (S 
+TMP_70) in (let TMP_72 \def (trans hds0 i) in (let TMP_73 \def (S TMP_72) in 
+(let TMP_74 \def (minus d TMP_73) in (let TMP_75 \def (plus TMP_71 TMP_74) in 
+(let TMP_91 \def (\lambda (n: nat).(let TMP_76 \def (trans hds0 i) in (let 
+TMP_77 \def (S TMP_76) in (let TMP_78 \def (ptrans hds0 i) in (let TMP_79 
+\def (lift1 TMP_78 t) in (let TMP_80 \def (lift TMP_77 O TMP_79) in (let 
+TMP_81 \def (lift h n TMP_80) in (let TMP_82 \def (trans hds0 i) in (let 
+TMP_83 \def (S TMP_82) in (let TMP_84 \def (trans hds0 i) in (let TMP_85 \def 
+(S TMP_84) in (let TMP_86 \def (minus d TMP_85) in (let TMP_87 \def (ptrans 
+hds0 i) in (let TMP_88 \def (PCons h TMP_86 TMP_87) in (let TMP_89 \def 
+(lift1 TMP_88 t) in (let TMP_90 \def (lift TMP_83 O TMP_89) in (eq T TMP_81 
+TMP_90))))))))))))))))) in (let TMP_92 \def (trans hds0 i) in (let TMP_93 
+\def (S TMP_92) in (let TMP_94 \def (trans hds0 i) in (let TMP_95 \def (S 
+TMP_94) in (let TMP_96 \def (minus d TMP_95) in (let TMP_97 \def (ptrans hds0 
+i) in (let TMP_98 \def (lift1 TMP_97 t) in (let TMP_99 \def (lift h TMP_96 
+TMP_98) in (let TMP_100 \def (lift TMP_93 O TMP_99) in (let TMP_110 \def 
+(\lambda (t0: T).(let TMP_101 \def (trans hds0 i) in (let TMP_102 \def (S 
+TMP_101) in (let TMP_103 \def (trans hds0 i) in (let TMP_104 \def (S TMP_103) 
+in (let TMP_105 \def (minus d TMP_104) in (let TMP_106 \def (ptrans hds0 i) 
+in (let TMP_107 \def (PCons h TMP_105 TMP_106) in (let TMP_108 \def (lift1 
+TMP_107 t) in (let TMP_109 \def (lift TMP_102 O TMP_108) in (eq T t0 
+TMP_109))))))))))) in (let TMP_111 \def (trans hds0 i) in (let TMP_112 \def 
+(S TMP_111) in (let TMP_113 \def (trans hds0 i) in (let TMP_114 \def (S 
+TMP_113) in (let TMP_115 \def (minus d TMP_114) in (let TMP_116 \def (ptrans 
+hds0 i) in (let TMP_117 \def (PCons h TMP_115 TMP_116) in (let TMP_118 \def 
+(lift1 TMP_117 t) in (let TMP_119 \def (lift TMP_112 O TMP_118) in (let 
+TMP_120 \def (refl_equal T TMP_119) in (let TMP_121 \def (trans hds0 i) in 
+(let TMP_122 \def (S TMP_121) in (let TMP_123 \def (trans hds0 i) in (let 
+TMP_124 \def (S TMP_123) in (let TMP_125 \def (minus d TMP_124) in (let 
+TMP_126 \def (plus TMP_122 TMP_125) in (let TMP_127 \def (trans hds0 i) in 
+(let TMP_128 \def (S TMP_127) in (let TMP_129 \def (ptrans hds0 i) in (let 
+TMP_130 \def (lift1 TMP_129 t) in (let TMP_131 \def (lift TMP_128 O TMP_130) 
+in (let TMP_132 \def (lift h TMP_126 TMP_131) in (let TMP_133 \def (ptrans 
+hds0 i) in (let TMP_134 \def (lift1 TMP_133 t) in (let TMP_135 \def (trans 
+hds0 i) in (let TMP_136 \def (S TMP_135) in (let TMP_137 \def (trans hds0 i) 
+in (let TMP_138 \def (S TMP_137) in (let TMP_139 \def (minus d TMP_138) in 
+(let TMP_140 \def (trans hds0 i) in (let TMP_141 \def (S TMP_140) in (let 
+TMP_142 \def (minus d TMP_141) in (let TMP_143 \def (le_O_n TMP_142) in (let 
+TMP_144 \def (lift_d TMP_134 h TMP_136 TMP_139 O TMP_143) in (let TMP_145 
+\def (eq_ind_r T TMP_100 TMP_110 TMP_120 TMP_132 TMP_144) in (let TMP_146 
+\def (trans hds0 i) in (let TMP_147 \def (S TMP_146) in (let TMP_148 \def 
+(trans hds0 i) in (let TMP_149 \def (S TMP_148) in (let TMP_150 \def (trans 
+hds0 i) in (let TMP_151 \def (S TMP_150) in (let TMP_152 \def (trans hds0 i) 
+in (let TMP_153 \def (trans hds0 i) in (let TMP_154 \def (blt_lt d TMP_153 
+H0) in (let TMP_155 \def (lt_le_S TMP_152 d TMP_154) in (let TMP_156 \def 
+(le_bge TMP_151 d TMP_155) in (let TMP_157 \def (bge_le TMP_149 d TMP_156) in 
+(let TMP_158 \def (le_plus_minus TMP_147 d TMP_157) in (eq_ind_r nat TMP_75 
+TMP_91 TMP_145 d 
+TMP_158))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in 
+(let TMP_255 \def (\lambda (H0: (eq bool (blt (trans hds0 i) d) false)).(let 
+TMP_160 \def (trans hds0 i) in (let TMP_161 \def (S TMP_160) in (let TMP_162 
+\def (plus h TMP_161) in (let TMP_163 \def (ptrans hds0 i) in (let TMP_164 
+\def (lift1 TMP_163 t) in (let TMP_165 \def (lift TMP_162 O TMP_164) in (let 
+TMP_172 \def (\lambda (t0: T).(let TMP_166 \def (trans hds0 i) in (let 
+TMP_167 \def (plus TMP_166 h) in (let TMP_168 \def (S TMP_167) in (let 
+TMP_169 \def (ptrans hds0 i) in (let TMP_170 \def (lift1 TMP_169 t) in (let 
+TMP_171 \def (lift TMP_168 O TMP_170) in (eq T t0 TMP_171)))))))) in (let 
+TMP_173 \def (trans hds0 i) in (let TMP_174 \def (plus h TMP_173) in (let 
+TMP_175 \def (S TMP_174) in (let TMP_185 \def (\lambda (n: nat).(let TMP_176 
+\def (ptrans hds0 i) in (let TMP_177 \def (lift1 TMP_176 t) in (let TMP_178 
+\def (lift n O TMP_177) in (let TMP_179 \def (trans hds0 i) in (let TMP_180 
+\def (plus TMP_179 h) in (let TMP_181 \def (S TMP_180) in (let TMP_182 \def 
+(ptrans hds0 i) in (let TMP_183 \def (lift1 TMP_182 t) in (let TMP_184 \def 
+(lift TMP_181 O TMP_183) in (eq T TMP_178 TMP_184))))))))))) in (let TMP_186 
+\def (trans hds0 i) in (let TMP_187 \def (plus TMP_186 h) in (let TMP_198 
+\def (\lambda (n: nat).(let TMP_188 \def (S n) in (let TMP_189 \def (ptrans 
+hds0 i) in (let TMP_190 \def (lift1 TMP_189 t) in (let TMP_191 \def (lift 
+TMP_188 O TMP_190) in (let TMP_192 \def (trans hds0 i) in (let TMP_193 \def 
+(plus TMP_192 h) in (let TMP_194 \def (S TMP_193) in (let TMP_195 \def 
+(ptrans hds0 i) in (let TMP_196 \def (lift1 TMP_195 t) in (let TMP_197 \def 
+(lift TMP_194 O TMP_196) in (eq T TMP_191 TMP_197)))))))))))) in (let TMP_199 
+\def (trans hds0 i) in (let TMP_200 \def (plus TMP_199 h) in (let TMP_201 
+\def (S TMP_200) in (let TMP_202 \def (ptrans hds0 i) in (let TMP_203 \def 
+(lift1 TMP_202 t) in (let TMP_204 \def (lift TMP_201 O TMP_203) in (let 
+TMP_205 \def (refl_equal T TMP_204) in (let TMP_206 \def (trans hds0 i) in 
+(let TMP_207 \def (plus h TMP_206) in (let TMP_208 \def (trans hds0 i) in 
+(let TMP_209 \def (plus_sym h TMP_208) in (let TMP_210 \def (eq_ind_r nat 
+TMP_187 TMP_198 TMP_205 TMP_207 TMP_209) in (let TMP_211 \def (trans hds0 i) 
+in (let TMP_212 \def (S TMP_211) in (let TMP_213 \def (plus h TMP_212) in 
+(let TMP_214 \def (trans hds0 i) in (let TMP_215 \def (plus_n_Sm h TMP_214) 
+in (let TMP_216 \def (eq_ind nat TMP_175 TMP_185 TMP_210 TMP_213 TMP_215) in 
+(let TMP_217 \def (trans hds0 i) in (let TMP_218 \def (S TMP_217) in (let 
+TMP_219 \def (ptrans hds0 i) in (let TMP_220 \def (lift1 TMP_219 t) in (let 
+TMP_221 \def (lift TMP_218 O TMP_220) in (let TMP_222 \def (lift h d TMP_221) 
+in (let TMP_223 \def (ptrans hds0 i) in (let TMP_224 \def (lift1 TMP_223 t) 
+in (let TMP_225 \def (trans hds0 i) in (let TMP_226 \def (S TMP_225) in (let 
+TMP_227 \def (trans hds0 i) in (let TMP_228 \def (plus O TMP_227) in (let 
+TMP_229 \def (S TMP_228) in (let TMP_230 \def (\lambda (n: nat).(le d n)) in 
+(let TMP_231 \def (trans hds0 i) in (let TMP_232 \def (plus TMP_231 O) in 
+(let TMP_234 \def (\lambda (n: nat).(let TMP_233 \def (S n) in (le d 
+TMP_233))) in (let TMP_235 \def (trans hds0 i) in (let TMP_236 \def (plus 
+TMP_235 O) in (let TMP_237 \def (trans hds0 i) in (let TMP_238 \def (trans 
+hds0 i) in (let TMP_239 \def (bge_le d TMP_238 H0) in (let TMP_240 \def 
+(le_plus_trans d TMP_237 O TMP_239) in (let TMP_241 \def (le_S d TMP_236 
+TMP_240) in (let TMP_242 \def (trans hds0 i) in (let TMP_243 \def (plus O 
+TMP_242) in (let TMP_244 \def (trans hds0 i) in (let TMP_245 \def (plus_sym O 
+TMP_244) in (let TMP_246 \def (eq_ind_r nat TMP_232 TMP_234 TMP_241 TMP_243 
+TMP_245) in (let TMP_247 \def (trans hds0 i) in (let TMP_248 \def (S TMP_247) 
+in (let TMP_249 \def (plus O TMP_248) in (let TMP_250 \def (trans hds0 i) in 
+(let TMP_251 \def (plus_n_Sm O TMP_250) in (let TMP_252 \def (eq_ind nat 
+TMP_229 TMP_230 TMP_246 TMP_249 TMP_251) in (let TMP_253 \def (le_O_n d) in 
+(let TMP_254 \def (lift_free TMP_224 TMP_226 h O d TMP_252 TMP_253) in 
+(eq_ind_r T TMP_165 TMP_172 TMP_216 TMP_222 
+TMP_254)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+ in (bool_ind TMP_69 TMP_159 TMP_255 x_x))))) in (let TMP_257 \def 
+(xinduction bool TMP_35 TMP_52 TMP_256) in (let TMP_258 \def (S i) in (let 
+TMP_259 \def (lift TMP_258 O t) in (let TMP_260 \def (lift1 hds0 TMP_259) in 
+(let TMP_261 \def (H i t) in (eq_ind_r T TMP_17 TMP_33 TMP_257 TMP_260 
+TMP_261)))))))))))))))))))))) in (PList_ind TMP_9 TMP_12 TMP_262 hds)))).
+

diff --git a/matita/matita/contribs/lambdadelta/basic_1/lift1/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/lift1/fwd.ma
deleted file mode 100644 (file)
index e9ae2d1..0000000
--- a/matita/matita/contribs/lambdadelta/basic_1/lift1/fwd.ma
+++ /dev/null
@@ -1,164 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* This file was automatically generated: do not edit *********************)
-
-include "Basic-1/lift1/defs.ma".
-
-include "Basic-1/lift/fwd.ma".
-
-theorem lift1_sort:
- \forall (n: nat).(\forall (is: PList).(eq T (lift1 is (TSort n)) (TSort n)))
-\def
- \lambda (n: nat).(\lambda (is: PList).(PList_ind (\lambda (p: PList).(eq T 
-(lift1 p (TSort n)) (TSort n))) (refl_equal T (TSort n)) (\lambda (n0: 
-nat).(\lambda (n1: nat).(\lambda (p: PList).(\lambda (H: (eq T (lift1 p 
-(TSort n)) (TSort n))).(eq_ind_r T (TSort n) (\lambda (t: T).(eq T (lift n0 
-n1 t) (TSort n))) (refl_equal T (TSort n)) (lift1 p (TSort n)) H))))) is)).
-(* COMMENTS
-Initial nodes: 99
-END *)
-
-theorem lift1_lref:
- \forall (hds: PList).(\forall (i: nat).(eq T (lift1 hds (TLRef i)) (TLRef 
-(trans hds i))))
-\def
- \lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (i: nat).(eq T 
-(lift1 p (TLRef i)) (TLRef (trans p i))))) (\lambda (i: nat).(refl_equal T 
-(TLRef i))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda 
-(H: ((\forall (i: nat).(eq T (lift1 p (TLRef i)) (TLRef (trans p 
-i)))))).(\lambda (i: nat).(eq_ind_r T (TLRef (trans p i)) (\lambda (t: T).(eq 
-T (lift n n0 t) (TLRef (match (blt (trans p i) n0) with [true \Rightarrow 
-(trans p i) | false \Rightarrow (plus (trans p i) n)])))) (refl_equal T 
-(TLRef (match (blt (trans p i) n0) with [true \Rightarrow (trans p i) | false 
-\Rightarrow (plus (trans p i) n)]))) (lift1 p (TLRef i)) (H i))))))) hds).
-(* COMMENTS
-Initial nodes: 165
-END *)
-
-theorem lift1_bind:
- \forall (b: B).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T 
-(lift1 hds (THead (Bind b) u t)) (THead (Bind b) (lift1 hds u) (lift1 (Ss 
-hds) t))))))
-\def
- \lambda (b: B).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall 
-(u: T).(\forall (t: T).(eq T (lift1 p (THead (Bind b) u t)) (THead (Bind b) 
-(lift1 p u) (lift1 (Ss p) t)))))) (\lambda (u: T).(\lambda (t: T).(refl_equal 
-T (THead (Bind b) u t)))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: 
-PList).(\lambda (H: ((\forall (u: T).(\forall (t: T).(eq T (lift1 p (THead 
-(Bind b) u t)) (THead (Bind b) (lift1 p u) (lift1 (Ss p) t))))))).(\lambda 
-(u: T).(\lambda (t: T).(eq_ind_r T (THead (Bind b) (lift1 p u) (lift1 (Ss p) 
-t)) (\lambda (t0: T).(eq T (lift n n0 t0) (THead (Bind b) (lift n n0 (lift1 p 
-u)) (lift n (S n0) (lift1 (Ss p) t))))) (eq_ind_r T (THead (Bind b) (lift n 
-n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t))) (\lambda (t0: T).(eq T t0 
-(THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t))))) 
-(refl_equal T (THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1 
-(Ss p) t)))) (lift n n0 (THead (Bind b) (lift1 p u) (lift1 (Ss p) t))) 
-(lift_bind b (lift1 p u) (lift1 (Ss p) t) n n0)) (lift1 p (THead (Bind b) u 
-t)) (H u t)))))))) hds)).
-(* COMMENTS
-Initial nodes: 379
-END *)
-
-theorem lift1_flat:
- \forall (f: F).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T 
-(lift1 hds (THead (Flat f) u t)) (THead (Flat f) (lift1 hds u) (lift1 hds 
-t))))))
-\def
- \lambda (f: F).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall 
-(u: T).(\forall (t: T).(eq T (lift1 p (THead (Flat f) u t)) (THead (Flat f) 
-(lift1 p u) (lift1 p t)))))) (\lambda (u: T).(\lambda (t: T).(refl_equal T 
-(THead (Flat f) u t)))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: 
-PList).(\lambda (H: ((\forall (u: T).(\forall (t: T).(eq T (lift1 p (THead 
-(Flat f) u t)) (THead (Flat f) (lift1 p u) (lift1 p t))))))).(\lambda (u: 
-T).(\lambda (t: T).(eq_ind_r T (THead (Flat f) (lift1 p u) (lift1 p t)) 
-(\lambda (t0: T).(eq T (lift n n0 t0) (THead (Flat f) (lift n n0 (lift1 p u)) 
-(lift n n0 (lift1 p t))))) (eq_ind_r T (THead (Flat f) (lift n n0 (lift1 p 
-u)) (lift n n0 (lift1 p t))) (\lambda (t0: T).(eq T t0 (THead (Flat f) (lift 
-n n0 (lift1 p u)) (lift n n0 (lift1 p t))))) (refl_equal T (THead (Flat f) 
-(lift n n0 (lift1 p u)) (lift n n0 (lift1 p t)))) (lift n n0 (THead (Flat f) 
-(lift1 p u) (lift1 p t))) (lift_flat f (lift1 p u) (lift1 p t) n n0)) (lift1 
-p (THead (Flat f) u t)) (H u t)))))))) hds)).
-(* COMMENTS
-Initial nodes: 353
-END *)
-
-theorem lift1_cons_tail:
- \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(eq 
-T (lift1 (PConsTail hds h d) t) (lift1 hds (lift h d t))))))
-\def
- \lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (hds: 
-PList).(PList_ind (\lambda (p: PList).(eq T (lift1 (PConsTail p h d) t) 
-(lift1 p (lift h d t)))) (refl_equal T (lift h d t)) (\lambda (n: 
-nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H: (eq T (lift1 
-(PConsTail p h d) t) (lift1 p (lift h d t)))).(eq_ind_r T (lift1 p (lift h d 
-t)) (\lambda (t0: T).(eq T (lift n n0 t0) (lift n n0 (lift1 p (lift h d 
-t))))) (refl_equal T (lift n n0 (lift1 p (lift h d t)))) (lift1 (PConsTail p 
-h d) t) H))))) hds)))).
-(* COMMENTS
-Initial nodes: 171
-END *)
-
-theorem lifts1_flat:
- \forall (f: F).(\forall (hds: PList).(\forall (t: T).(\forall (ts: 
-TList).(eq T (lift1 hds (THeads (Flat f) ts t)) (THeads (Flat f) (lifts1 hds 
-ts) (lift1 hds t))))))
-\def
- \lambda (f: F).(\lambda (hds: PList).(\lambda (t: T).(\lambda (ts: 
-TList).(TList_ind (\lambda (t0: TList).(eq T (lift1 hds (THeads (Flat f) t0 
-t)) (THeads (Flat f) (lifts1 hds t0) (lift1 hds t)))) (refl_equal T (lift1 
-hds t)) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (H: (eq T (lift1 hds 
-(THeads (Flat f) t1 t)) (THeads (Flat f) (lifts1 hds t1) (lift1 hds 
-t)))).(eq_ind_r T (THead (Flat f) (lift1 hds t0) (lift1 hds (THeads (Flat f) 
-t1 t))) (\lambda (t2: T).(eq T t2 (THead (Flat f) (lift1 hds t0) (THeads 
-(Flat f) (lifts1 hds t1) (lift1 hds t))))) (eq_ind_r T (THeads (Flat f) 
-(lifts1 hds t1) (lift1 hds t)) (\lambda (t2: T).(eq T (THead (Flat f) (lift1 
-hds t0) t2) (THead (Flat f) (lift1 hds t0) (THeads (Flat f) (lifts1 hds t1) 
-(lift1 hds t))))) (refl_equal T (THead (Flat f) (lift1 hds t0) (THeads (Flat 
-f) (lifts1 hds t1) (lift1 hds t)))) (lift1 hds (THeads (Flat f) t1 t)) H) 
-(lift1 hds (THead (Flat f) t0 (THeads (Flat f) t1 t))) (lift1_flat f hds t0 
-(THeads (Flat f) t1 t)))))) ts)))).
-(* COMMENTS
-Initial nodes: 329
-END *)
-
-theorem lifts1_nil:
- \forall (ts: TList).(eq TList (lifts1 PNil ts) ts)
-\def
- \lambda (ts: TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 PNil t) 
-t)) (refl_equal TList TNil) (\lambda (t: T).(\lambda (t0: TList).(\lambda (H: 
-(eq TList (lifts1 PNil t0) t0)).(eq_ind_r TList t0 (\lambda (t1: TList).(eq 
-TList (TCons t t1) (TCons t t0))) (refl_equal TList (TCons t t0)) (lifts1 
-PNil t0) H)))) ts).
-(* COMMENTS
-Initial nodes: 83
-END *)
-
-theorem lifts1_cons:
- \forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(\forall (ts: 
-TList).(eq TList (lifts1 (PCons h d hds) ts) (lifts h d (lifts1 hds ts))))))
-\def
- \lambda (h: nat).(\lambda (d: nat).(\lambda (hds: PList).(\lambda (ts: 
-TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 (PCons h d hds) t) 
-(lifts h d (lifts1 hds t)))) (refl_equal TList TNil) (\lambda (t: T).(\lambda 
-(t0: TList).(\lambda (H: (eq TList (lifts1 (PCons h d hds) t0) (lifts h d 
-(lifts1 hds t0)))).(eq_ind_r TList (lifts h d (lifts1 hds t0)) (\lambda (t1: 
-TList).(eq TList (TCons (lift h d (lift1 hds t)) t1) (TCons (lift h d (lift1 
-hds t)) (lifts h d (lifts1 hds t0))))) (refl_equal TList (TCons (lift h d 
-(lift1 hds t)) (lifts h d (lifts1 hds t0)))) (lifts1 (PCons h d hds) t0) 
-H)))) ts)))).
-(* COMMENTS
-Initial nodes: 187
-END *)
-

diff --git a/matita/matita/contribs/lambdadelta/basic_1/lift1/props.ma b/matita/matita/contribs/lambdadelta/basic_1/lift1/props.ma
index ebda0267b48515dad8367c3aa7ee12d1145946c5..bb6374c163e23e6d07af085837a28ee81fb4a039 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/lift1/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/lift1/props.ma
@@ -14,126 +14,231 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/lift/props.ma".
+include "basic_1/lift1/defs.ma".
 
-include "Basic-1/drop1/defs.ma".
+include "basic_1/lift/props.ma".
 
-theorem lift1_lift1:
- \forall (is1: PList).(\forall (is2: PList).(\forall (t: T).(eq T (lift1 is1 
-(lift1 is2 t)) (lift1 (papp is1 is2) t))))
+theorem lift1_sort:
+ \forall (n: nat).(\forall (is: PList).(eq T (lift1 is (TSort n)) (TSort n)))
 \def
- \lambda (is1: PList).(PList_ind (\lambda (p: PList).(\forall (is2: 
-PList).(\forall (t: T).(eq T (lift1 p (lift1 is2 t)) (lift1 (papp p is2) 
-t))))) (\lambda (is2: PList).(\lambda (t: T).(refl_equal T (lift1 is2 t)))) 
-(\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H: 
-((\forall (is2: PList).(\forall (t: T).(eq T (lift1 p (lift1 is2 t)) (lift1 
-(papp p is2) t)))))).(\lambda (is2: PList).(\lambda (t: T).(f_equal3 nat nat 
-T T lift n n n0 n0 (lift1 p (lift1 is2 t)) (lift1 (papp p is2) t) (refl_equal 
-nat n) (refl_equal nat n0) (H is2 t)))))))) is1).
-(* COMMENTS
-Initial nodes: 145
-END *)
+ \lambda (n: nat).(\lambda (is: PList).(let TMP_4 \def (\lambda (p: 
+PList).(let TMP_1 \def (TSort n) in (let TMP_2 \def (lift1 p TMP_1) in (let 
+TMP_3 \def (TSort n) in (eq T TMP_2 TMP_3))))) in (let TMP_5 \def (TSort n) 
+in (let TMP_6 \def (refl_equal T TMP_5) in (let TMP_15 \def (\lambda (n0: 
+nat).(\lambda (n1: nat).(\lambda (p: PList).(\lambda (H: (eq T (lift1 p 
+(TSort n)) (TSort n))).(let TMP_7 \def (TSort n) in (let TMP_10 \def (\lambda 
+(t: T).(let TMP_8 \def (lift n0 n1 t) in (let TMP_9 \def (TSort n) in (eq T 
+TMP_8 TMP_9)))) in (let TMP_11 \def (TSort n) in (let TMP_12 \def (refl_equal 
+T TMP_11) in (let TMP_13 \def (TSort n) in (let TMP_14 \def (lift1 p TMP_13) 
+in (eq_ind_r T TMP_7 TMP_10 TMP_12 TMP_14 H))))))))))) in (PList_ind TMP_4 
+TMP_6 TMP_15 is)))))).
 
-theorem lift1_xhg:
- \forall (hds: PList).(\forall (t: T).(eq T (lift1 (Ss hds) (lift (S O) O t)) 
-(lift (S O) O (lift1 hds t))))
+theorem lift1_lref:
+ \forall (hds: PList).(\forall (i: nat).(eq T (lift1 hds (TLRef i)) (TLRef 
+(trans hds i))))
 \def
- \lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (t: T).(eq T 
-(lift1 (Ss p) (lift (S O) O t)) (lift (S O) O (lift1 p t))))) (\lambda (t: 
-T).(refl_equal T (lift (S O) O t))) (\lambda (h: nat).(\lambda (d: 
-nat).(\lambda (p: PList).(\lambda (H: ((\forall (t: T).(eq T (lift1 (Ss p) 
-(lift (S O) O t)) (lift (S O) O (lift1 p t)))))).(\lambda (t: T).(eq_ind_r T 
-(lift (S O) O (lift1 p t)) (\lambda (t0: T).(eq T (lift h (S d) t0) (lift (S 
-O) O (lift h d (lift1 p t))))) (eq_ind nat (plus (S O) d) (\lambda (n: 
-nat).(eq T (lift h n (lift (S O) O (lift1 p t))) (lift (S O) O (lift h d 
-(lift1 p t))))) (eq_ind_r T (lift (S O) O (lift h d (lift1 p t))) (\lambda 
-(t0: T).(eq T t0 (lift (S O) O (lift h d (lift1 p t))))) (refl_equal T (lift 
-(S O) O (lift h d (lift1 p t)))) (lift h (plus (S O) d) (lift (S O) O (lift1 
-p t))) (lift_d (lift1 p t) h (S O) d O (le_O_n d))) (S d) (refl_equal nat (S 
-d))) (lift1 (Ss p) (lift (S O) O t)) (H t))))))) hds).
-(* COMMENTS
-Initial nodes: 371
-END *)
+ \lambda (hds: PList).(let TMP_5 \def (\lambda (p: PList).(\forall (i: 
+nat).(let TMP_1 \def (TLRef i) in (let TMP_2 \def (lift1 p TMP_1) in (let 
+TMP_3 \def (trans p i) in (let TMP_4 \def (TLRef TMP_3) in (eq T TMP_2 
+TMP_4))))))) in (let TMP_7 \def (\lambda (i: nat).(let TMP_6 \def (TLRef i) 
+in (refl_equal T TMP_6))) in (let TMP_26 \def (\lambda (n: nat).(\lambda (n0: 
+nat).(\lambda (p: PList).(\lambda (H: ((\forall (i: nat).(eq T (lift1 p 
+(TLRef i)) (TLRef (trans p i)))))).(\lambda (i: nat).(let TMP_8 \def (trans p 
+i) in (let TMP_9 \def (TLRef TMP_8) in (let TMP_16 \def (\lambda (t: T).(let 
+TMP_10 \def (lift n n0 t) in (let TMP_11 \def (trans p i) in (let TMP_12 \def 
+(blt TMP_11 n0) in (let TMP_14 \def (match TMP_12 with [true \Rightarrow 
+(trans p i) | false \Rightarrow (let TMP_13 \def (trans p i) in (plus TMP_13 
+n))]) in (let TMP_15 \def (TLRef TMP_14) in (eq T TMP_10 TMP_15))))))) in 
+(let TMP_17 \def (trans p i) in (let TMP_18 \def (blt TMP_17 n0) in (let 
+TMP_20 \def (match TMP_18 with [true \Rightarrow (trans p i) | false 
+\Rightarrow (let TMP_19 \def (trans p i) in (plus TMP_19 n))]) in (let TMP_21 
+\def (TLRef TMP_20) in (let TMP_22 \def (refl_equal T TMP_21) in (let TMP_23 
+\def (TLRef i) in (let TMP_24 \def (lift1 p TMP_23) in (let TMP_25 \def (H i) 
+in (eq_ind_r T TMP_9 TMP_16 TMP_22 TMP_24 TMP_25))))))))))))))))) in 
+(PList_ind TMP_5 TMP_7 TMP_26 hds)))).
 
-theorem lifts1_xhg:
- \forall (hds: PList).(\forall (ts: TList).(eq TList (lifts1 (Ss hds) (lifts 
-(S O) O ts)) (lifts (S O) O (lifts1 hds ts))))
+theorem lift1_bind:
+ \forall (b: B).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T 
+(lift1 hds (THead (Bind b) u t)) (THead (Bind b) (lift1 hds u) (lift1 (Ss 
+hds) t))))))
 \def
- \lambda (hds: PList).(\lambda (ts: TList).(TList_ind (\lambda (t: TList).(eq 
-TList (lifts1 (Ss hds) (lifts (S O) O t)) (lifts (S O) O (lifts1 hds t)))) 
-(refl_equal TList TNil) (\lambda (t: T).(\lambda (t0: TList).(\lambda (H: (eq 
-TList (lifts1 (Ss hds) (lifts (S O) O t0)) (lifts (S O) O (lifts1 hds 
-t0)))).(eq_ind_r T (lift (S O) O (lift1 hds t)) (\lambda (t1: T).(eq TList 
-(TCons t1 (lifts1 (Ss hds) (lifts (S O) O t0))) (TCons (lift (S O) O (lift1 
-hds t)) (lifts (S O) O (lifts1 hds t0))))) (eq_ind_r TList (lifts (S O) O 
-(lifts1 hds t0)) (\lambda (t1: TList).(eq TList (TCons (lift (S O) O (lift1 
-hds t)) t1) (TCons (lift (S O) O (lift1 hds t)) (lifts (S O) O (lifts1 hds 
-t0))))) (refl_equal TList (TCons (lift (S O) O (lift1 hds t)) (lifts (S O) O 
-(lifts1 hds t0)))) (lifts1 (Ss hds) (lifts (S O) O t0)) H) (lift1 (Ss hds) 
-(lift (S O) O t)) (lift1_xhg hds t))))) ts)).
-(* COMMENTS
-Initial nodes: 307
-END *)
+ \lambda (b: B).(\lambda (hds: PList).(let TMP_9 \def (\lambda (p: 
+PList).(\forall (u: T).(\forall (t: T).(let TMP_1 \def (Bind b) in (let TMP_2 
+\def (THead TMP_1 u t) in (let TMP_3 \def (lift1 p TMP_2) in (let TMP_4 \def 
+(Bind b) in (let TMP_5 \def (lift1 p u) in (let TMP_6 \def (Ss p) in (let 
+TMP_7 \def (lift1 TMP_6 t) in (let TMP_8 \def (THead TMP_4 TMP_5 TMP_7) in 
+(eq T TMP_3 TMP_8)))))))))))) in (let TMP_12 \def (\lambda (u: T).(\lambda 
+(t: T).(let TMP_10 \def (Bind b) in (let TMP_11 \def (THead TMP_10 u t) in 
+(refl_equal T TMP_11))))) in (let TMP_69 \def (\lambda (n: nat).(\lambda (n0: 
+nat).(\lambda (p: PList).(\lambda (H: ((\forall (u: T).(\forall (t: T).(eq T 
+(lift1 p (THead (Bind b) u t)) (THead (Bind b) (lift1 p u) (lift1 (Ss p) 
+t))))))).(\lambda (u: T).(\lambda (t: T).(let TMP_13 \def (Bind b) in (let 
+TMP_14 \def (lift1 p u) in (let TMP_15 \def (Ss p) in (let TMP_16 \def (lift1 
+TMP_15 t) in (let TMP_17 \def (THead TMP_13 TMP_14 TMP_16) in (let TMP_27 
+\def (\lambda (t0: T).(let TMP_18 \def (lift n n0 t0) in (let TMP_19 \def 
+(Bind b) in (let TMP_20 \def (lift1 p u) in (let TMP_21 \def (lift n n0 
+TMP_20) in (let TMP_22 \def (S n0) in (let TMP_23 \def (Ss p) in (let TMP_24 
+\def (lift1 TMP_23 t) in (let TMP_25 \def (lift n TMP_22 TMP_24) in (let 
+TMP_26 \def (THead TMP_19 TMP_21 TMP_25) in (eq T TMP_18 TMP_26))))))))))) in 
+(let TMP_28 \def (Bind b) in (let TMP_29 \def (lift1 p u) in (let TMP_30 \def 
+(lift n n0 TMP_29) in (let TMP_31 \def (S n0) in (let TMP_32 \def (Ss p) in 
+(let TMP_33 \def (lift1 TMP_32 t) in (let TMP_34 \def (lift n TMP_31 TMP_33) 
+in (let TMP_35 \def (THead TMP_28 TMP_30 TMP_34) in (let TMP_44 \def (\lambda 
+(t0: T).(let TMP_36 \def (Bind b) in (let TMP_37 \def (lift1 p u) in (let 
+TMP_38 \def (lift n n0 TMP_37) in (let TMP_39 \def (S n0) in (let TMP_40 \def 
+(Ss p) in (let TMP_41 \def (lift1 TMP_40 t) in (let TMP_42 \def (lift n 
+TMP_39 TMP_41) in (let TMP_43 \def (THead TMP_36 TMP_38 TMP_42) in (eq T t0 
+TMP_43)))))))))) in (let TMP_45 \def (Bind b) in (let TMP_46 \def (lift1 p u) 
+in (let TMP_47 \def (lift n n0 TMP_46) in (let TMP_48 \def (S n0) in (let 
+TMP_49 \def (Ss p) in (let TMP_50 \def (lift1 TMP_49 t) in (let TMP_51 \def 
+(lift n TMP_48 TMP_50) in (let TMP_52 \def (THead TMP_45 TMP_47 TMP_51) in 
+(let TMP_53 \def (refl_equal T TMP_52) in (let TMP_54 \def (Bind b) in (let 
+TMP_55 \def (lift1 p u) in (let TMP_56 \def (Ss p) in (let TMP_57 \def (lift1 
+TMP_56 t) in (let TMP_58 \def (THead TMP_54 TMP_55 TMP_57) in (let TMP_59 
+\def (lift n n0 TMP_58) in (let TMP_60 \def (lift1 p u) in (let TMP_61 \def 
+(Ss p) in (let TMP_62 \def (lift1 TMP_61 t) in (let TMP_63 \def (lift_bind b 
+TMP_60 TMP_62 n n0) in (let TMP_64 \def (eq_ind_r T TMP_35 TMP_44 TMP_53 
+TMP_59 TMP_63) in (let TMP_65 \def (Bind b) in (let TMP_66 \def (THead TMP_65 
+u t) in (let TMP_67 \def (lift1 p TMP_66) in (let TMP_68 \def (H u t) in 
+(eq_ind_r T TMP_17 TMP_27 TMP_64 TMP_67 
+TMP_68)))))))))))))))))))))))))))))))))))))))))))))) in (PList_ind TMP_9 
+TMP_12 TMP_69 hds))))).
 
-theorem lift1_free:
- \forall (hds: PList).(\forall (i: nat).(\forall (t: T).(eq T (lift1 hds 
-(lift (S i) O t)) (lift (S (trans hds i)) O (lift1 (ptrans hds i) t)))))
+theorem lift1_flat:
+ \forall (f: F).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T 
+(lift1 hds (THead (Flat f) u t)) (THead (Flat f) (lift1 hds u) (lift1 hds 
+t))))))
 \def
- \lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (i: 
-nat).(\forall (t: T).(eq T (lift1 p (lift (S i) O t)) (lift (S (trans p i)) O 
-(lift1 (ptrans p i) t)))))) (\lambda (i: nat).(\lambda (t: T).(refl_equal T 
-(lift (S i) O t)))) (\lambda (h: nat).(\lambda (d: nat).(\lambda (hds0: 
-PList).(\lambda (H: ((\forall (i: nat).(\forall (t: T).(eq T (lift1 hds0 
-(lift (S i) O t)) (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) 
-t))))))).(\lambda (i: nat).(\lambda (t: T).(eq_ind_r T (lift (S (trans hds0 
-i)) O (lift1 (ptrans hds0 i) t)) (\lambda (t0: T).(eq T (lift h d t0) (lift 
-(S (match (blt (trans hds0 i) d) with [true \Rightarrow (trans hds0 i) | 
-false \Rightarrow (plus (trans hds0 i) h)])) O (lift1 (match (blt (trans hds0 
-i) d) with [true \Rightarrow (PCons h (minus d (S (trans hds0 i))) (ptrans 
-hds0 i)) | false \Rightarrow (ptrans hds0 i)]) t)))) (xinduction bool (blt 
-(trans hds0 i) d) (\lambda (b: bool).(eq T (lift h d (lift (S (trans hds0 i)) 
-O (lift1 (ptrans hds0 i) t))) (lift (S (match b with [true \Rightarrow (trans 
-hds0 i) | false \Rightarrow (plus (trans hds0 i) h)])) O (lift1 (match b with 
-[true \Rightarrow (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) | 
-false \Rightarrow (ptrans hds0 i)]) t)))) (\lambda (x_x: bool).(bool_ind 
-(\lambda (b: bool).((eq bool (blt (trans hds0 i) d) b) \to (eq T (lift h d 
-(lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t))) (lift (S (match b with 
-[true \Rightarrow (trans hds0 i) | false \Rightarrow (plus (trans hds0 i) 
-h)])) O (lift1 (match b with [true \Rightarrow (PCons h (minus d (S (trans 
-hds0 i))) (ptrans hds0 i)) | false \Rightarrow (ptrans hds0 i)]) t))))) 
-(\lambda (H0: (eq bool (blt (trans hds0 i) d) true)).(eq_ind_r nat (plus (S 
-(trans hds0 i)) (minus d (S (trans hds0 i)))) (\lambda (n: nat).(eq T (lift h 
-n (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t))) (lift (S (trans hds0 
-i)) O (lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) t)))) 
-(eq_ind_r T (lift (S (trans hds0 i)) O (lift h (minus d (S (trans hds0 i))) 
-(lift1 (ptrans hds0 i) t))) (\lambda (t0: T).(eq T t0 (lift (S (trans hds0 
-i)) O (lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) t)))) 
-(refl_equal T (lift (S (trans hds0 i)) O (lift1 (PCons h (minus d (S (trans 
-hds0 i))) (ptrans hds0 i)) t))) (lift h (plus (S (trans hds0 i)) (minus d (S 
-(trans hds0 i)))) (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t))) 
-(lift_d (lift1 (ptrans hds0 i) t) h (S (trans hds0 i)) (minus d (S (trans 
-hds0 i))) O (le_O_n (minus d (S (trans hds0 i)))))) d (le_plus_minus (S 
-(trans hds0 i)) d (bge_le (S (trans hds0 i)) d (le_bge (S (trans hds0 i)) d 
-(lt_le_S (trans hds0 i) d (blt_lt d (trans hds0 i) H0))))))) (\lambda (H0: 
-(eq bool (blt (trans hds0 i) d) false)).(eq_ind_r T (lift (plus h (S (trans 
-hds0 i))) O (lift1 (ptrans hds0 i) t)) (\lambda (t0: T).(eq T t0 (lift (S 
-(plus (trans hds0 i) h)) O (lift1 (ptrans hds0 i) t)))) (eq_ind nat (S (plus 
-h (trans hds0 i))) (\lambda (n: nat).(eq T (lift n O (lift1 (ptrans hds0 i) 
-t)) (lift (S (plus (trans hds0 i) h)) O (lift1 (ptrans hds0 i) t)))) 
-(eq_ind_r nat (plus (trans hds0 i) h) (\lambda (n: nat).(eq T (lift (S n) O 
-(lift1 (ptrans hds0 i) t)) (lift (S (plus (trans hds0 i) h)) O (lift1 (ptrans 
-hds0 i) t)))) (refl_equal T (lift (S (plus (trans hds0 i) h)) O (lift1 
-(ptrans hds0 i) t))) (plus h (trans hds0 i)) (plus_sym h (trans hds0 i))) 
-(plus h (S (trans hds0 i))) (plus_n_Sm h (trans hds0 i))) (lift h d (lift (S 
-(trans hds0 i)) O (lift1 (ptrans hds0 i) t))) (lift_free (lift1 (ptrans hds0 
-i) t) (S (trans hds0 i)) h O d (eq_ind nat (S (plus O (trans hds0 i))) 
-(\lambda (n: nat).(le d n)) (eq_ind_r nat (plus (trans hds0 i) O) (\lambda 
-(n: nat).(le d (S n))) (le_S d (plus (trans hds0 i) O) (le_plus_trans d 
-(trans hds0 i) O (bge_le d (trans hds0 i) H0))) (plus O (trans hds0 i)) 
-(plus_sym O (trans hds0 i))) (plus O (S (trans hds0 i))) (plus_n_Sm O (trans 
-hds0 i))) (le_O_n d)))) x_x))) (lift1 hds0 (lift (S i) O t)) (H i t)))))))) 
-hds).
-(* COMMENTS
-Initial nodes: 1339
-END *)
+ \lambda (f: F).(\lambda (hds: PList).(let TMP_8 \def (\lambda (p: 
+PList).(\forall (u: T).(\forall (t: T).(let TMP_1 \def (Flat f) in (let TMP_2 
+\def (THead TMP_1 u t) in (let TMP_3 \def (lift1 p TMP_2) in (let TMP_4 \def 
+(Flat f) in (let TMP_5 \def (lift1 p u) in (let TMP_6 \def (lift1 p t) in 
+(let TMP_7 \def (THead TMP_4 TMP_5 TMP_6) in (eq T TMP_3 TMP_7))))))))))) in 
+(let TMP_11 \def (\lambda (u: T).(\lambda (t: T).(let TMP_9 \def (Flat f) in 
+(let TMP_10 \def (THead TMP_9 u t) in (refl_equal T TMP_10))))) in (let 
+TMP_57 \def (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda 
+(H: ((\forall (u: T).(\forall (t: T).(eq T (lift1 p (THead (Flat f) u t)) 
+(THead (Flat f) (lift1 p u) (lift1 p t))))))).(\lambda (u: T).(\lambda (t: 
+T).(let TMP_12 \def (Flat f) in (let TMP_13 \def (lift1 p u) in (let TMP_14 
+\def (lift1 p t) in (let TMP_15 \def (THead TMP_12 TMP_13 TMP_14) in (let 
+TMP_23 \def (\lambda (t0: T).(let TMP_16 \def (lift n n0 t0) in (let TMP_17 
+\def (Flat f) in (let TMP_18 \def (lift1 p u) in (let TMP_19 \def (lift n n0 
+TMP_18) in (let TMP_20 \def (lift1 p t) in (let TMP_21 \def (lift n n0 
+TMP_20) in (let TMP_22 \def (THead TMP_17 TMP_19 TMP_21) in (eq T TMP_16 
+TMP_22))))))))) in (let TMP_24 \def (Flat f) in (let TMP_25 \def (lift1 p u) 
+in (let TMP_26 \def (lift n n0 TMP_25) in (let TMP_27 \def (lift1 p t) in 
+(let TMP_28 \def (lift n n0 TMP_27) in (let TMP_29 \def (THead TMP_24 TMP_26 
+TMP_28) in (let TMP_36 \def (\lambda (t0: T).(let TMP_30 \def (Flat f) in 
+(let TMP_31 \def (lift1 p u) in (let TMP_32 \def (lift n n0 TMP_31) in (let 
+TMP_33 \def (lift1 p t) in (let TMP_34 \def (lift n n0 TMP_33) in (let TMP_35 
+\def (THead TMP_30 TMP_32 TMP_34) in (eq T t0 TMP_35)))))))) in (let TMP_37 
+\def (Flat f) in (let TMP_38 \def (lift1 p u) in (let TMP_39 \def (lift n n0 
+TMP_38) in (let TMP_40 \def (lift1 p t) in (let TMP_41 \def (lift n n0 
+TMP_40) in (let TMP_42 \def (THead TMP_37 TMP_39 TMP_41) in (let TMP_43 \def 
+(refl_equal T TMP_42) in (let TMP_44 \def (Flat f) in (let TMP_45 \def (lift1 
+p u) in (let TMP_46 \def (lift1 p t) in (let TMP_47 \def (THead TMP_44 TMP_45 
+TMP_46) in (let TMP_48 \def (lift n n0 TMP_47) in (let TMP_49 \def (lift1 p 
+u) in (let TMP_50 \def (lift1 p t) in (let TMP_51 \def (lift_flat f TMP_49 
+TMP_50 n n0) in (let TMP_52 \def (eq_ind_r T TMP_29 TMP_36 TMP_43 TMP_48 
+TMP_51) in (let TMP_53 \def (Flat f) in (let TMP_54 \def (THead TMP_53 u t) 
+in (let TMP_55 \def (lift1 p TMP_54) in (let TMP_56 \def (H u t) in (eq_ind_r 
+T TMP_15 TMP_23 TMP_52 TMP_55 TMP_56))))))))))))))))))))))))))))))))))))))) 
+in (PList_ind TMP_8 TMP_11 TMP_57 hds))))).
+
+theorem lift1_cons_tail:
+ \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(eq 
+T (lift1 (PConsTail hds h d) t) (lift1 hds (lift h d t))))))
+\def
+ \lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (hds: 
+PList).(let TMP_5 \def (\lambda (p: PList).(let TMP_1 \def (PConsTail p h d) 
+in (let TMP_2 \def (lift1 TMP_1 t) in (let TMP_3 \def (lift h d t) in (let 
+TMP_4 \def (lift1 p TMP_3) in (eq T TMP_2 TMP_4)))))) in (let TMP_6 \def 
+(lift h d t) in (let TMP_7 \def (refl_equal T TMP_6) in (let TMP_21 \def 
+(\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H: (eq T 
+(lift1 (PConsTail p h d) t) (lift1 p (lift h d t)))).(let TMP_8 \def (lift h 
+d t) in (let TMP_9 \def (lift1 p TMP_8) in (let TMP_14 \def (\lambda (t0: 
+T).(let TMP_10 \def (lift n n0 t0) in (let TMP_11 \def (lift h d t) in (let 
+TMP_12 \def (lift1 p TMP_11) in (let TMP_13 \def (lift n n0 TMP_12) in (eq T 
+TMP_10 TMP_13)))))) in (let TMP_15 \def (lift h d t) in (let TMP_16 \def 
+(lift1 p TMP_15) in (let TMP_17 \def (lift n n0 TMP_16) in (let TMP_18 \def 
+(refl_equal T TMP_17) in (let TMP_19 \def (PConsTail p h d) in (let TMP_20 
+\def (lift1 TMP_19 t) in (eq_ind_r T TMP_9 TMP_14 TMP_18 TMP_20 
+H)))))))))))))) in (PList_ind TMP_5 TMP_7 TMP_21 hds)))))))).
+
+theorem lifts1_flat:
+ \forall (f: F).(\forall (hds: PList).(\forall (t: T).(\forall (ts: 
+TList).(eq T (lift1 hds (THeads (Flat f) ts t)) (THeads (Flat f) (lifts1 hds 
+ts) (lift1 hds t))))))
+\def
+ \lambda (f: F).(\lambda (hds: PList).(\lambda (t: T).(\lambda (ts: 
+TList).(let TMP_8 \def (\lambda (t0: TList).(let TMP_1 \def (Flat f) in (let 
+TMP_2 \def (THeads TMP_1 t0 t) in (let TMP_3 \def (lift1 hds TMP_2) in (let 
+TMP_4 \def (Flat f) in (let TMP_5 \def (lifts1 hds t0) in (let TMP_6 \def 
+(lift1 hds t) in (let TMP_7 \def (THeads TMP_4 TMP_5 TMP_6) in (eq T TMP_3 
+TMP_7))))))))) in (let TMP_9 \def (lift1 hds t) in (let TMP_10 \def 
+(refl_equal T TMP_9) in (let TMP_60 \def (\lambda (t0: T).(\lambda (t1: 
+TList).(\lambda (H: (eq T (lift1 hds (THeads (Flat f) t1 t)) (THeads (Flat f) 
+(lifts1 hds t1) (lift1 hds t)))).(let TMP_11 \def (Flat f) in (let TMP_12 
+\def (lift1 hds t0) in (let TMP_13 \def (Flat f) in (let TMP_14 \def (THeads 
+TMP_13 t1 t) in (let TMP_15 \def (lift1 hds TMP_14) in (let TMP_16 \def 
+(THead TMP_11 TMP_12 TMP_15) in (let TMP_24 \def (\lambda (t2: T).(let TMP_17 
+\def (Flat f) in (let TMP_18 \def (lift1 hds t0) in (let TMP_19 \def (Flat f) 
+in (let TMP_20 \def (lifts1 hds t1) in (let TMP_21 \def (lift1 hds t) in (let 
+TMP_22 \def (THeads TMP_19 TMP_20 TMP_21) in (let TMP_23 \def (THead TMP_17 
+TMP_18 TMP_22) in (eq T t2 TMP_23))))))))) in (let TMP_25 \def (Flat f) in 
+(let TMP_26 \def (lifts1 hds t1) in (let TMP_27 \def (lift1 hds t) in (let 
+TMP_28 \def (THeads TMP_25 TMP_26 TMP_27) in (let TMP_39 \def (\lambda (t2: 
+T).(let TMP_29 \def (Flat f) in (let TMP_30 \def (lift1 hds t0) in (let 
+TMP_31 \def (THead TMP_29 TMP_30 t2) in (let TMP_32 \def (Flat f) in (let 
+TMP_33 \def (lift1 hds t0) in (let TMP_34 \def (Flat f) in (let TMP_35 \def 
+(lifts1 hds t1) in (let TMP_36 \def (lift1 hds t) in (let TMP_37 \def (THeads 
+TMP_34 TMP_35 TMP_36) in (let TMP_38 \def (THead TMP_32 TMP_33 TMP_37) in (eq 
+T TMP_31 TMP_38)))))))))))) in (let TMP_40 \def (Flat f) in (let TMP_41 \def 
+(lift1 hds t0) in (let TMP_42 \def (Flat f) in (let TMP_43 \def (lifts1 hds 
+t1) in (let TMP_44 \def (lift1 hds t) in (let TMP_45 \def (THeads TMP_42 
+TMP_43 TMP_44) in (let TMP_46 \def (THead TMP_40 TMP_41 TMP_45) in (let 
+TMP_47 \def (refl_equal T TMP_46) in (let TMP_48 \def (Flat f) in (let TMP_49 
+\def (THeads TMP_48 t1 t) in (let TMP_50 \def (lift1 hds TMP_49) in (let 
+TMP_51 \def (eq_ind_r T TMP_28 TMP_39 TMP_47 TMP_50 H) in (let TMP_52 \def 
+(Flat f) in (let TMP_53 \def (Flat f) in (let TMP_54 \def (THeads TMP_53 t1 
+t) in (let TMP_55 \def (THead TMP_52 t0 TMP_54) in (let TMP_56 \def (lift1 
+hds TMP_55) in (let TMP_57 \def (Flat f) in (let TMP_58 \def (THeads TMP_57 
+t1 t) in (let TMP_59 \def (lift1_flat f hds t0 TMP_58) in (eq_ind_r T TMP_16 
+TMP_24 TMP_51 TMP_56 TMP_59)))))))))))))))))))))))))))))))))))) in (TList_ind 
+TMP_8 TMP_10 TMP_60 ts)))))))).
+
+theorem lifts1_nil:
+ \forall (ts: TList).(eq TList (lifts1 PNil ts) ts)
+\def
+ \lambda (ts: TList).(let TMP_2 \def (\lambda (t: TList).(let TMP_1 \def 
+(lifts1 PNil t) in (eq TList TMP_1 t))) in (let TMP_3 \def (refl_equal TList 
+TNil) in (let TMP_10 \def (\lambda (t: T).(\lambda (t0: TList).(\lambda (H: 
+(eq TList (lifts1 PNil t0) t0)).(let TMP_6 \def (\lambda (t1: TList).(let 
+TMP_4 \def (TCons t t1) in (let TMP_5 \def (TCons t t0) in (eq TList TMP_4 
+TMP_5)))) in (let TMP_7 \def (TCons t t0) in (let TMP_8 \def (refl_equal 
+TList TMP_7) in (let TMP_9 \def (lifts1 PNil t0) in (eq_ind_r TList t0 TMP_6 
+TMP_8 TMP_9 H)))))))) in (TList_ind TMP_2 TMP_3 TMP_10 ts)))).
+
+theorem lifts1_cons:
+ \forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(\forall (ts: 
+TList).(eq TList (lifts1 (PCons h d hds) ts) (lifts h d (lifts1 hds ts))))))
+\def
+ \lambda (h: nat).(\lambda (d: nat).(\lambda (hds: PList).(\lambda (ts: 
+TList).(let TMP_5 \def (\lambda (t: TList).(let TMP_1 \def (PCons h d hds) in 
+(let TMP_2 \def (lifts1 TMP_1 t) in (let TMP_3 \def (lifts1 hds t) in (let 
+TMP_4 \def (lifts h d TMP_3) in (eq TList TMP_2 TMP_4)))))) in (let TMP_6 
+\def (refl_equal TList TNil) in (let TMP_26 \def (\lambda (t: T).(\lambda 
+(t0: TList).(\lambda (H: (eq TList (lifts1 (PCons h d hds) t0) (lifts h d 
+(lifts1 hds t0)))).(let TMP_7 \def (lifts1 hds t0) in (let TMP_8 \def (lifts 
+h d TMP_7) in (let TMP_17 \def (\lambda (t1: TList).(let TMP_9 \def (lift1 
+hds t) in (let TMP_10 \def (lift h d TMP_9) in (let TMP_11 \def (TCons TMP_10 
+t1) in (let TMP_12 \def (lift1 hds t) in (let TMP_13 \def (lift h d TMP_12) 
+in (let TMP_14 \def (lifts1 hds t0) in (let TMP_15 \def (lifts h d TMP_14) in 
+(let TMP_16 \def (TCons TMP_13 TMP_15) in (eq TList TMP_11 TMP_16)))))))))) 
+in (let TMP_18 \def (lift1 hds t) in (let TMP_19 \def (lift h d TMP_18) in 
+(let TMP_20 \def (lifts1 hds t0) in (let TMP_21 \def (lifts h d TMP_20) in 
+(let TMP_22 \def (TCons TMP_19 TMP_21) in (let TMP_23 \def (refl_equal TList 
+TMP_22) in (let TMP_24 \def (PCons h d hds) in (let TMP_25 \def (lifts1 
+TMP_24 t0) in (eq_ind_r TList TMP_8 TMP_17 TMP_23 TMP_25 H))))))))))))))) in 
+(TList_ind TMP_5 TMP_6 TMP_26 ts))))))).