X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fsubst0%2Fprops.ma;h=762f857620b7b76de4419d69abaf4ae08330e9cf;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=04300ba9b17940db2d474d76edb124b2ad637d46;hpb=112d29685ee9dceff93cdf64867a1a8037a53842;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/subst0/props.ma b/matita/matita/contribs/lambdadelta/basic_1/subst0/props.ma
index 04300ba9b..762f85762 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/subst0/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/subst0/props.ma
@@ -16,405 +16,204 @@
 
 include "basic_1/subst0/fwd.ma".
 
-theorem subst0_refl:
+lemma subst0_refl:
  \forall (u: T).(\forall (t: T).(\forall (d: nat).((subst0 d u t t) \to 
 (\forall (P: Prop).P))))
 \def
- \lambda (u: T).(\lambda (t: T).(let TMP_1 \def (\lambda (t0: T).(\forall (d: 
-nat).((subst0 d u t0 t0) \to (\forall (P: Prop).P)))) in (let TMP_3 \def 
-(\lambda (n: nat).(\lambda (d: nat).(\lambda (H: (subst0 d u (TSort n) (TSort 
-n))).(\lambda (P: Prop).(let TMP_2 \def (TSort n) in (subst0_gen_sort u TMP_2 
-d n H P)))))) in (let TMP_17 \def (\lambda (n: nat).(\lambda (d: 
-nat).(\lambda (H: (subst0 d u (TLRef n) (TLRef n))).(\lambda (P: Prop).(let 
-TMP_4 \def (eq nat n d) in (let TMP_5 \def (TLRef n) in (let TMP_6 \def (S n) 
-in (let TMP_7 \def (lift TMP_6 O u) in (let TMP_8 \def (eq T TMP_5 TMP_7) in 
-(let TMP_14 \def (\lambda (_: (eq nat n d)).(\lambda (H1: (eq T (TLRef n) 
-(lift (S n) O u))).(let TMP_9 \def (S n) in (let TMP_10 \def (le_O_n n) in 
-(let TMP_11 \def (S n) in (let TMP_12 \def (plus O TMP_11) in (let TMP_13 
-\def (le_n TMP_12) in (lift_gen_lref_false TMP_9 O n TMP_10 TMP_13 u H1 
-P)))))))) in (let TMP_15 \def (TLRef n) in (let TMP_16 \def (subst0_gen_lref 
-u TMP_15 d n H) in (land_ind TMP_4 TMP_8 P TMP_14 TMP_16))))))))))))) in (let 
-TMP_79 \def (\lambda (k: K).(\lambda (t0: T).(\lambda (H: ((\forall (d: 
-nat).((subst0 d u t0 t0) \to (\forall (P: Prop).P))))).(\lambda (t1: 
-T).(\lambda (H0: ((\forall (d: nat).((subst0 d u t1 t1) \to (\forall (P: 
-Prop).P))))).(\lambda (d: nat).(\lambda (H1: (subst0 d u (THead k t0 t1) 
-(THead k t0 t1))).(\lambda (P: Prop).(let TMP_20 \def (\lambda (u2: T).(let 
-TMP_18 \def (THead k t0 t1) in (let TMP_19 \def (THead k u2 t1) in (eq T 
-TMP_18 TMP_19)))) in (let TMP_21 \def (\lambda (u2: T).(subst0 d u t0 u2)) in 
-(let TMP_22 \def (ex2 T TMP_20 TMP_21) in (let TMP_25 \def (\lambda (t2: 
-T).(let TMP_23 \def (THead k t0 t1) in (let TMP_24 \def (THead k t0 t2) in 
-(eq T TMP_23 TMP_24)))) in (let TMP_27 \def (\lambda (t2: T).(let TMP_26 \def 
-(s k d) in (subst0 TMP_26 u t1 t2))) in (let TMP_28 \def (ex2 T TMP_25 
-TMP_27) in (let TMP_31 \def (\lambda (u2: T).(\lambda (t2: T).(let TMP_29 
-\def (THead k t0 t1) in (let TMP_30 \def (THead k u2 t2) in (eq T TMP_29 
-TMP_30))))) in (let TMP_32 \def (\lambda (u2: T).(\lambda (_: T).(subst0 d u 
-t0 u2))) in (let TMP_34 \def (\lambda (_: T).(\lambda (t2: T).(let TMP_33 
-\def (s k d) in (subst0 TMP_33 u t1 t2)))) in (let TMP_35 \def (ex3_2 T T 
-TMP_31 TMP_32 TMP_34) in (let TMP_45 \def (\lambda (H2: (ex2 T (\lambda (u2: 
-T).(eq T (THead k t0 t1) (THead k u2 t1))) (\lambda (u2: T).(subst0 d u t0 
-u2)))).(let TMP_38 \def (\lambda (u2: T).(let TMP_36 \def (THead k t0 t1) in 
-(let TMP_37 \def (THead k u2 t1) in (eq T TMP_36 TMP_37)))) in (let TMP_39 
-\def (\lambda (u2: T).(subst0 d u t0 u2)) in (let TMP_44 \def (\lambda (x: 
-T).(\lambda (H3: (eq T (THead k t0 t1) (THead k x t1))).(\lambda (H4: (subst0 
-d u t0 x)).(let TMP_40 \def (\lambda (e: T).(match e with [(TSort _) 
-\Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ t2 _) \Rightarrow t2])) 
-in (let TMP_41 \def (THead k t0 t1) in (let TMP_42 \def (THead k x t1) in 
-(let H5 \def (f_equal T T TMP_40 TMP_41 TMP_42 H3) in (let TMP_43 \def 
-(\lambda (t2: T).(subst0 d u t0 t2)) in (let H6 \def (eq_ind_r T x TMP_43 H4 
-t0 H5) in (H d H6 P)))))))))) in (ex2_ind T TMP_38 TMP_39 P TMP_44 H2))))) in 
-(let TMP_58 \def (\lambda (H2: (ex2 T (\lambda (t2: T).(eq T (THead k t0 t1) 
-(THead k t0 t2))) (\lambda (t2: T).(subst0 (s k d) u t1 t2)))).(let TMP_48 
-\def (\lambda (t2: T).(let TMP_46 \def (THead k t0 t1) in (let TMP_47 \def 
-(THead k t0 t2) in (eq T TMP_46 TMP_47)))) in (let TMP_50 \def (\lambda (t2: 
-T).(let TMP_49 \def (s k d) in (subst0 TMP_49 u t1 t2))) in (let TMP_57 \def 
-(\lambda (x: T).(\lambda (H3: (eq T (THead k t0 t1) (THead k t0 x))).(\lambda 
-(H4: (subst0 (s k d) u t1 x)).(let TMP_51 \def (\lambda (e: T).(match e with 
+ \lambda (u: T).(\lambda (t: T).(T_ind (\lambda (t0: T).(\forall (d: 
+nat).((subst0 d u t0 t0) \to (\forall (P: Prop).P)))) (\lambda (n: 
+nat).(\lambda (d: nat).(\lambda (H: (subst0 d u (TSort n) (TSort 
+n))).(\lambda (P: Prop).(subst0_gen_sort u (TSort n) d n H P))))) (\lambda 
+(n: nat).(\lambda (d: nat).(\lambda (H: (subst0 d u (TLRef n) (TLRef 
+n))).(\lambda (P: Prop).(land_ind (eq nat n d) (eq T (TLRef n) (lift (S n) O 
+u)) P (\lambda (_: (eq nat n d)).(\lambda (H1: (eq T (TLRef n) (lift (S n) O 
+u))).(lift_gen_lref_false (S n) O n (le_O_n n) (le_n (plus O (S n))) u H1 
+P))) (subst0_gen_lref u (TLRef n) d n H)))))) (\lambda (k: K).(\lambda (t0: 
+T).(\lambda (H: ((\forall (d: nat).((subst0 d u t0 t0) \to (\forall (P: 
+Prop).P))))).(\lambda (t1: T).(\lambda (H0: ((\forall (d: nat).((subst0 d u 
+t1 t1) \to (\forall (P: Prop).P))))).(\lambda (d: nat).(\lambda (H1: (subst0 
+d u (THead k t0 t1) (THead k t0 t1))).(\lambda (P: Prop).(or3_ind (ex2 T 
+(\lambda (u2: T).(eq T (THead k t0 t1) (THead k u2 t1))) (\lambda (u2: 
+T).(subst0 d u t0 u2))) (ex2 T (\lambda (t2: T).(eq T (THead k t0 t1) (THead 
+k t0 t2))) (\lambda (t2: T).(subst0 (s k d) u t1 t2))) (ex3_2 T T (\lambda 
+(u2: T).(\lambda (t2: T).(eq T (THead k t0 t1) (THead k u2 t2)))) (\lambda 
+(u2: T).(\lambda (_: T).(subst0 d u t0 u2))) (\lambda (_: T).(\lambda (t2: 
+T).(subst0 (s k d) u t1 t2)))) P (\lambda (H2: (ex2 T (\lambda (u2: T).(eq T 
+(THead k t0 t1) (THead k u2 t1))) (\lambda (u2: T).(subst0 d u t0 
+u2)))).(ex2_ind T (\lambda (u2: T).(eq T (THead k t0 t1) (THead k u2 t1))) 
+(\lambda (u2: T).(subst0 d u t0 u2)) P (\lambda (x: T).(\lambda (H3: (eq T 
+(THead k t0 t1) (THead k x t1))).(\lambda (H4: (subst0 d u t0 x)).(let H5 
+\def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow t0 | 
+(TLRef _) \Rightarrow t0 | (THead _ t2 _) \Rightarrow t2])) (THead k t0 t1) 
+(THead k x t1) H3) in (let H6 \def (eq_ind_r T x (\lambda (t2: T).(subst0 d u 
+t0 t2)) H4 t0 H5) in (H d H6 P)))))) H2)) (\lambda (H2: (ex2 T (\lambda (t2: 
+T).(eq T (THead k t0 t1) (THead k t0 t2))) (\lambda (t2: T).(subst0 (s k d) u 
+t1 t2)))).(ex2_ind T (\lambda (t2: T).(eq T (THead k t0 t1) (THead k t0 t2))) 
+(\lambda (t2: T).(subst0 (s k d) u t1 t2)) P (\lambda (x: T).(\lambda (H3: 
+(eq T (THead k t0 t1) (THead k t0 x))).(\lambda (H4: (subst0 (s k d) u t1 
+x)).(let H5 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) 
+\Rightarrow t1 | (TLRef _) \Rightarrow t1 | (THead _ _ t2) \Rightarrow t2])) 
+(THead k t0 t1) (THead k t0 x) H3) in (let H6 \def (eq_ind_r T x (\lambda 
+(t2: T).(subst0 (s k d) u t1 t2)) H4 t1 H5) in (H0 (s k d) H6 P)))))) H2)) 
+(\lambda (H2: (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead k t0 
+t1) (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst0 d u t0 u2))) 
+(\lambda (_: T).(\lambda (t2: T).(subst0 (s k d) u t1 t2))))).(ex3_2_ind T T 
+(\lambda (u2: T).(\lambda (t2: T).(eq T (THead k t0 t1) (THead k u2 t2)))) 
+(\lambda (u2: T).(\lambda (_: T).(subst0 d u t0 u2))) (\lambda (_: 
+T).(\lambda (t2: T).(subst0 (s k d) u t1 t2))) P (\lambda (x0: T).(\lambda 
+(x1: T).(\lambda (H3: (eq T (THead k t0 t1) (THead k x0 x1))).(\lambda (H4: 
+(subst0 d u t0 x0)).(\lambda (H5: (subst0 (s k d) u t1 x1)).(let H6 \def 
+(f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow t0 | (TLRef 
+_) \Rightarrow t0 | (THead _ t2 _) \Rightarrow t2])) (THead k t0 t1) (THead k 
+x0 x1) H3) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e with 
 [(TSort _) \Rightarrow t1 | (TLRef _) \Rightarrow t1 | (THead _ _ t2) 
-\Rightarrow t2])) in (let TMP_52 \def (THead k t0 t1) in (let TMP_53 \def 
-(THead k t0 x) in (let H5 \def (f_equal T T TMP_51 TMP_52 TMP_53 H3) in (let 
-TMP_55 \def (\lambda (t2: T).(let TMP_54 \def (s k d) in (subst0 TMP_54 u t1 
-t2))) in (let H6 \def (eq_ind_r T x TMP_55 H4 t1 H5) in (let TMP_56 \def (s k 
-d) in (H0 TMP_56 H6 P))))))))))) in (ex2_ind T TMP_48 TMP_50 P TMP_57 H2))))) 
-in (let TMP_76 \def (\lambda (H2: (ex3_2 T T (\lambda (u2: T).(\lambda (t2: 
-T).(eq T (THead k t0 t1) (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: 
-T).(subst0 d u t0 u2))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k d) u t1 
-t2))))).(let TMP_61 \def (\lambda (u2: T).(\lambda (t2: T).(let TMP_59 \def 
-(THead k t0 t1) in (let TMP_60 \def (THead k u2 t2) in (eq T TMP_59 
-TMP_60))))) in (let TMP_62 \def (\lambda (u2: T).(\lambda (_: T).(subst0 d u 
-t0 u2))) in (let TMP_64 \def (\lambda (_: T).(\lambda (t2: T).(let TMP_63 
-\def (s k d) in (subst0 TMP_63 u t1 t2)))) in (let TMP_75 \def (\lambda (x0: 
-T).(\lambda (x1: T).(\lambda (H3: (eq T (THead k t0 t1) (THead k x0 
-x1))).(\lambda (H4: (subst0 d u t0 x0)).(\lambda (H5: (subst0 (s k d) u t1 
-x1)).(let TMP_65 \def (\lambda (e: T).(match e with [(TSort _) \Rightarrow t0 
-| (TLRef _) \Rightarrow t0 | (THead _ t2 _) \Rightarrow t2])) in (let TMP_66 
-\def (THead k t0 t1) in (let TMP_67 \def (THead k x0 x1) in (let H6 \def 
-(f_equal T T TMP_65 TMP_66 TMP_67 H3) in (let TMP_68 \def (\lambda (e: 
-T).(match e with [(TSort _) \Rightarrow t1 | (TLRef _) \Rightarrow t1 | 
-(THead _ _ t2) \Rightarrow t2])) in (let TMP_69 \def (THead k t0 t1) in (let 
-TMP_70 \def (THead k x0 x1) in (let H7 \def (f_equal T T TMP_68 TMP_69 TMP_70 
-H3) in (let TMP_74 \def (\lambda (H8: (eq T t0 x0)).(let TMP_72 \def (\lambda 
-(t2: T).(let TMP_71 \def (s k d) in (subst0 TMP_71 u t1 t2))) in (let H9 \def 
-(eq_ind_r T x1 TMP_72 H5 t1 H7) in (let TMP_73 \def (\lambda (t2: T).(subst0 
-d u t0 t2)) in (let H10 \def (eq_ind_r T x0 TMP_73 H4 t0 H8) in (H d H10 
-P)))))) in (TMP_74 H6))))))))))))))) in (ex3_2_ind T T TMP_61 TMP_62 TMP_64 P 
-TMP_75 H2)))))) in (let TMP_77 \def (THead k t0 t1) in (let TMP_78 \def 
-(subst0_gen_head k u t0 t1 TMP_77 d H1) in (or3_ind TMP_22 TMP_28 TMP_35 P 
-TMP_45 TMP_58 TMP_76 TMP_78)))))))))))))))))))))))) in (T_ind TMP_1 TMP_3 
-TMP_17 TMP_79 t)))))).
+\Rightarrow t2])) (THead k t0 t1) (THead k x0 x1) H3) in (\lambda (H8: (eq T 
+t0 x0)).(let H9 \def (eq_ind_r T x1 (\lambda (t2: T).(subst0 (s k d) u t1 
+t2)) H5 t1 H7) in (let H10 \def (eq_ind_r T x0 (\lambda (t2: T).(subst0 d u 
+t0 t2)) H4 t0 H8) in (H d H10 P))))) H6))))))) H2)) (subst0_gen_head k u t0 
+t1 (THead k t0 t1) d H1)))))))))) t)).
 
-theorem subst0_lift_lt:
+lemma subst0_lift_lt:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst0 
 i u t1 t2) \to (\forall (d: nat).((lt i d) \to (\forall (h: nat).(subst0 i 
 (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)))))))))
 \def
  \lambda (t1: T).(\lambda (t2: T).(\lambda (u: T).(\lambda (i: nat).(\lambda 
-(H: (subst0 i u t1 t2)).(let TMP_6 \def (\lambda (n: nat).(\lambda (t: 
+(H: (subst0 i u t1 t2)).(subst0_ind (\lambda (n: nat).(\lambda (t: 
 T).(\lambda (t0: T).(\lambda (t3: T).(\forall (d: nat).((lt n d) \to (\forall 
-(h: nat).(let TMP_1 \def (S n) in (let TMP_2 \def (minus d TMP_1) in (let 
-TMP_3 \def (lift h TMP_2 t) in (let TMP_4 \def (lift h d t0) in (let TMP_5 
-\def (lift h d t3) in (subst0 n TMP_3 TMP_4 TMP_5))))))))))))) in (let TMP_59 
-\def (\lambda (v: T).(\lambda (i0: nat).(\lambda (d: nat).(\lambda (H0: (lt 
-i0 d)).(\lambda (h: nat).(let TMP_7 \def (TLRef i0) in (let TMP_14 \def 
-(\lambda (t: T).(let TMP_8 \def (S i0) in (let TMP_9 \def (minus d TMP_8) in 
-(let TMP_10 \def (lift h TMP_9 v) in (let TMP_11 \def (S i0) in (let TMP_12 
-\def (lift TMP_11 O v) in (let TMP_13 \def (lift h d TMP_12) in (subst0 i0 
-TMP_10 t TMP_13)))))))) in (let TMP_15 \def (S i0) in (let w \def (minus d 
-TMP_15) in (let TMP_16 \def (S i0) in (let TMP_17 \def (S i0) in (let TMP_18 
-\def (minus d TMP_17) in (let TMP_19 \def (plus TMP_16 TMP_18) in (let TMP_25 
-\def (\lambda (n: nat).(let TMP_20 \def (lift h w v) in (let TMP_21 \def 
-(TLRef i0) in (let TMP_22 \def (S i0) in (let TMP_23 \def (lift TMP_22 O v) 
-in (let TMP_24 \def (lift h n TMP_23) in (subst0 i0 TMP_20 TMP_21 
-TMP_24))))))) in (let TMP_26 \def (S i0) in (let TMP_27 \def (S i0) in (let 
-TMP_28 \def (minus d TMP_27) in (let TMP_29 \def (lift h TMP_28 v) in (let 
-TMP_30 \def (lift TMP_26 O TMP_29) in (let TMP_33 \def (\lambda (t: T).(let 
-TMP_31 \def (lift h w v) in (let TMP_32 \def (TLRef i0) in (subst0 i0 TMP_31 
-TMP_32 t)))) in (let TMP_34 \def (S i0) in (let TMP_35 \def (minus d TMP_34) 
-in (let TMP_36 \def (lift h TMP_35 v) in (let TMP_37 \def (subst0_lref TMP_36 
-i0) in (let TMP_38 \def (S i0) in (let TMP_39 \def (S i0) in (let TMP_40 \def 
-(minus d TMP_39) in (let TMP_41 \def (plus TMP_38 TMP_40) in (let TMP_42 \def 
-(S i0) in (let TMP_43 \def (lift TMP_42 O v) in (let TMP_44 \def (lift h 
-TMP_41 TMP_43) in (let TMP_45 \def (S i0) in (let TMP_46 \def (S i0) in (let 
-TMP_47 \def (minus d TMP_46) in (let TMP_48 \def (S i0) in (let TMP_49 \def 
-(minus d TMP_48) in (let TMP_50 \def (le_O_n TMP_49) in (let TMP_51 \def 
-(lift_d v h TMP_45 TMP_47 O TMP_50) in (let TMP_52 \def (eq_ind_r T TMP_30 
-TMP_33 TMP_37 TMP_44 TMP_51) in (let TMP_53 \def (S i0) in (let TMP_54 \def 
-(le_plus_minus_r TMP_53 d H0) in (let TMP_55 \def (eq_ind nat TMP_19 TMP_25 
-TMP_52 d TMP_54) in (let TMP_56 \def (TLRef i0) in (let TMP_57 \def (lift h d 
-TMP_56) in (let TMP_58 \def (lift_lref_lt i0 h d H0) in (eq_ind_r T TMP_7 
-TMP_14 TMP_55 TMP_57 TMP_58)))))))))))))))))))))))))))))))))))))))))))))) in 
-(let TMP_98 \def (\lambda (v: T).(\lambda (u2: T).(\lambda (u1: T).(\lambda 
+(h: nat).(subst0 n (lift h (minus d (S n)) t) (lift h d t0) (lift h d 
+t3))))))))) (\lambda (v: T).(\lambda (i0: nat).(\lambda (d: nat).(\lambda 
+(H0: (lt i0 d)).(\lambda (h: nat).(eq_ind_r T (TLRef i0) (\lambda (t: 
+T).(subst0 i0 (lift h (minus d (S i0)) v) t (lift h d (lift (S i0) O v)))) 
+(let w \def (minus d (S i0)) in (eq_ind nat (plus (S i0) (minus d (S i0))) 
+(\lambda (n: nat).(subst0 i0 (lift h w v) (TLRef i0) (lift h n (lift (S i0) O 
+v)))) (eq_ind_r T (lift (S i0) O (lift h (minus d (S i0)) v)) (\lambda (t: 
+T).(subst0 i0 (lift h w v) (TLRef i0) t)) (subst0_lref (lift h (minus d (S 
+i0)) v) i0) (lift h (plus (S i0) (minus d (S i0))) (lift (S i0) O v)) (lift_d 
+v h (S i0) (minus d (S i0)) O (le_O_n (minus d (S i0))))) d (le_plus_minus_r 
+(S i0) d H0))) (lift h d (TLRef i0)) (lift_lref_lt i0 h d H0))))))) (\lambda 
+(v: T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i0: nat).(\lambda (_: 
+(subst0 i0 v u1 u2)).(\lambda (H1: ((\forall (d: nat).((lt i0 d) \to (\forall 
+(h: nat).(subst0 i0 (lift h (minus d (S i0)) v) (lift h d u1) (lift h d 
+u2))))))).(\lambda (t: T).(\lambda (k: K).(\lambda (d: nat).(\lambda (H2: (lt 
+i0 d)).(\lambda (h: nat).(eq_ind_r T (THead k (lift h d u1) (lift h (s k d) 
+t)) (\lambda (t0: T).(subst0 i0 (lift h (minus d (S i0)) v) t0 (lift h d 
+(THead k u2 t)))) (eq_ind_r T (THead k (lift h d u2) (lift h (s k d) t)) 
+(\lambda (t0: T).(subst0 i0 (lift h (minus d (S i0)) v) (THead k (lift h d 
+u1) (lift h (s k d) t)) t0)) (subst0_fst (lift h (minus d (S i0)) v) (lift h 
+d u2) (lift h d u1) i0 (H1 d H2 h) (lift h (s k d) t) k) (lift h d (THead k 
+u2 t)) (lift_head k u2 t h d)) (lift h d (THead k u1 t)) (lift_head k u1 t h 
+d))))))))))))) (\lambda (k: K).(\lambda (v: T).(\lambda (t0: T).(\lambda (t3: 
+T).(\lambda (i0: nat).(\lambda (_: (subst0 (s k i0) v t3 t0)).(\lambda (H1: 
+((\forall (d: nat).((lt (s k i0) d) \to (\forall (h: nat).(subst0 (s k i0) 
+(lift h (minus d (S (s k i0))) v) (lift h d t3) (lift h d t0))))))).(\lambda 
+(u0: T).(\lambda (d: nat).(\lambda (H2: (lt i0 d)).(\lambda (h: nat).(let H3 
+\def (eq_ind_r nat (S (s k i0)) (\lambda (n: nat).(\forall (d0: nat).((lt (s 
+k i0) d0) \to (\forall (h0: nat).(subst0 (s k i0) (lift h0 (minus d0 n) v) 
+(lift h0 d0 t3) (lift h0 d0 t0)))))) H1 (s k (S i0)) (s_S k i0)) in (eq_ind_r 
+T (THead k (lift h d u0) (lift h (s k d) t3)) (\lambda (t: T).(subst0 i0 
+(lift h (minus d (S i0)) v) t (lift h d (THead k u0 t0)))) (eq_ind_r T (THead 
+k (lift h d u0) (lift h (s k d) t0)) (\lambda (t: T).(subst0 i0 (lift h 
+(minus d (S i0)) v) (THead k (lift h d u0) (lift h (s k d) t3)) t)) (eq_ind 
+nat (minus (s k d) (s k (S i0))) (\lambda (n: nat).(subst0 i0 (lift h n v) 
+(THead k (lift h d u0) (lift h (s k d) t3)) (THead k (lift h d u0) (lift h (s 
+k d) t0)))) (subst0_snd k (lift h (minus (s k d) (s k (S i0))) v) (lift h (s 
+k d) t0) (lift h (s k d) t3) i0 (H3 (s k d) (s_lt k i0 d H2) h) (lift h d 
+u0)) (minus d (S i0)) (minus_s_s k d (S i0))) (lift h d (THead k u0 t0)) 
+(lift_head k u0 t0 h d)) (lift h d (THead k u0 t3)) (lift_head k u0 t3 h 
+d)))))))))))))) (\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda 
 (i0: nat).(\lambda (_: (subst0 i0 v u1 u2)).(\lambda (H1: ((\forall (d: 
 nat).((lt i0 d) \to (\forall (h: nat).(subst0 i0 (lift h (minus d (S i0)) v) 
-(lift h d u1) (lift h d u2))))))).(\lambda (t: T).(\lambda (k: K).(\lambda 
-(d: nat).(\lambda (H2: (lt i0 d)).(\lambda (h: nat).(let TMP_60 \def (lift h 
-d u1) in (let TMP_61 \def (s k d) in (let TMP_62 \def (lift h TMP_61 t) in 
-(let TMP_63 \def (THead k TMP_60 TMP_62) in (let TMP_69 \def (\lambda (t0: 
-T).(let TMP_64 \def (S i0) in (let TMP_65 \def (minus d TMP_64) in (let 
-TMP_66 \def (lift h TMP_65 v) in (let TMP_67 \def (THead k u2 t) in (let 
-TMP_68 \def (lift h d TMP_67) in (subst0 i0 TMP_66 t0 TMP_68))))))) in (let 
-TMP_70 \def (lift h d u2) in (let TMP_71 \def (s k d) in (let TMP_72 \def 
-(lift h TMP_71 t) in (let TMP_73 \def (THead k TMP_70 TMP_72) in (let TMP_81 
-\def (\lambda (t0: T).(let TMP_74 \def (S i0) in (let TMP_75 \def (minus d 
-TMP_74) in (let TMP_76 \def (lift h TMP_75 v) in (let TMP_77 \def (lift h d 
-u1) in (let TMP_78 \def (s k d) in (let TMP_79 \def (lift h TMP_78 t) in (let 
-TMP_80 \def (THead k TMP_77 TMP_79) in (subst0 i0 TMP_76 TMP_80 t0))))))))) 
-in (let TMP_82 \def (S i0) in (let TMP_83 \def (minus d TMP_82) in (let 
-TMP_84 \def (lift h TMP_83 v) in (let TMP_85 \def (lift h d u2) in (let 
-TMP_86 \def (lift h d u1) in (let TMP_87 \def (H1 d H2 h) in (let TMP_88 \def 
-(s k d) in (let TMP_89 \def (lift h TMP_88 t) in (let TMP_90 \def (subst0_fst 
-TMP_84 TMP_85 TMP_86 i0 TMP_87 TMP_89 k) in (let TMP_91 \def (THead k u2 t) 
-in (let TMP_92 \def (lift h d TMP_91) in (let TMP_93 \def (lift_head k u2 t h 
-d) in (let TMP_94 \def (eq_ind_r T TMP_73 TMP_81 TMP_90 TMP_92 TMP_93) in 
-(let TMP_95 \def (THead k u1 t) in (let TMP_96 \def (lift h d TMP_95) in (let 
-TMP_97 \def (lift_head k u1 t h d) in (eq_ind_r T TMP_63 TMP_69 TMP_94 TMP_96 
-TMP_97)))))))))))))))))))))))))))))))))))))) in (let TMP_172 \def (\lambda 
-(k: K).(\lambda (v: T).(\lambda (t0: T).(\lambda (t3: T).(\lambda (i0: 
-nat).(\lambda (_: (subst0 (s k i0) v t3 t0)).(\lambda (H1: ((\forall (d: 
-nat).((lt (s k i0) d) \to (\forall (h: nat).(subst0 (s k i0) (lift h (minus d 
-(S (s k i0))) v) (lift h d t3) (lift h d t0))))))).(\lambda (u0: T).(\lambda 
-(d: nat).(\lambda (H2: (lt i0 d)).(\lambda (h: nat).(let TMP_99 \def (s k i0) 
-in (let TMP_100 \def (S TMP_99) in (let TMP_106 \def (\lambda (n: 
-nat).(\forall (d0: nat).((lt (s k i0) d0) \to (\forall (h0: nat).(let TMP_101 
-\def (s k i0) in (let TMP_102 \def (minus d0 n) in (let TMP_103 \def (lift h0 
-TMP_102 v) in (let TMP_104 \def (lift h0 d0 t3) in (let TMP_105 \def (lift h0 
-d0 t0) in (subst0 TMP_101 TMP_103 TMP_104 TMP_105)))))))))) in (let TMP_107 
-\def (S i0) in (let TMP_108 \def (s k TMP_107) in (let TMP_109 \def (s_S k 
-i0) in (let H3 \def (eq_ind_r nat TMP_100 TMP_106 H1 TMP_108 TMP_109) in (let 
-TMP_110 \def (lift h d u0) in (let TMP_111 \def (s k d) in (let TMP_112 \def 
-(lift h TMP_111 t3) in (let TMP_113 \def (THead k TMP_110 TMP_112) in (let 
-TMP_119 \def (\lambda (t: T).(let TMP_114 \def (S i0) in (let TMP_115 \def 
-(minus d TMP_114) in (let TMP_116 \def (lift h TMP_115 v) in (let TMP_117 
-\def (THead k u0 t0) in (let TMP_118 \def (lift h d TMP_117) in (subst0 i0 
-TMP_116 t TMP_118))))))) in (let TMP_120 \def (lift h d u0) in (let TMP_121 
-\def (s k d) in (let TMP_122 \def (lift h TMP_121 t0) in (let TMP_123 \def 
-(THead k TMP_120 TMP_122) in (let TMP_131 \def (\lambda (t: T).(let TMP_124 
-\def (S i0) in (let TMP_125 \def (minus d TMP_124) in (let TMP_126 \def (lift 
-h TMP_125 v) in (let TMP_127 \def (lift h d u0) in (let TMP_128 \def (s k d) 
-in (let TMP_129 \def (lift h TMP_128 t3) in (let TMP_130 \def (THead k 
-TMP_127 TMP_129) in (subst0 i0 TMP_126 TMP_130 t))))))))) in (let TMP_132 
-\def (s k d) in (let TMP_133 \def (S i0) in (let TMP_134 \def (s k TMP_133) 
-in (let TMP_135 \def (minus TMP_132 TMP_134) in (let TMP_145 \def (\lambda 
-(n: nat).(let TMP_136 \def (lift h n v) in (let TMP_137 \def (lift h d u0) in 
-(let TMP_138 \def (s k d) in (let TMP_139 \def (lift h TMP_138 t3) in (let 
-TMP_140 \def (THead k TMP_137 TMP_139) in (let TMP_141 \def (lift h d u0) in 
-(let TMP_142 \def (s k d) in (let TMP_143 \def (lift h TMP_142 t0) in (let 
-TMP_144 \def (THead k TMP_141 TMP_143) in (subst0 i0 TMP_136 TMP_140 
-TMP_144))))))))))) in (let TMP_146 \def (s k d) in (let TMP_147 \def (S i0) 
-in (let TMP_148 \def (s k TMP_147) in (let TMP_149 \def (minus TMP_146 
-TMP_148) in (let TMP_150 \def (lift h TMP_149 v) in (let TMP_151 \def (s k d) 
-in (let TMP_152 \def (lift h TMP_151 t0) in (let TMP_153 \def (s k d) in (let 
-TMP_154 \def (lift h TMP_153 t3) in (let TMP_155 \def (s k d) in (let TMP_156 
-\def (s_lt k i0 d H2) in (let TMP_157 \def (H3 TMP_155 TMP_156 h) in (let 
-TMP_158 \def (lift h d u0) in (let TMP_159 \def (subst0_snd k TMP_150 TMP_152 
-TMP_154 i0 TMP_157 TMP_158) in (let TMP_160 \def (S i0) in (let TMP_161 \def 
-(minus d TMP_160) in (let TMP_162 \def (S i0) in (let TMP_163 \def (minus_s_s 
-k d TMP_162) in (let TMP_164 \def (eq_ind nat TMP_135 TMP_145 TMP_159 TMP_161 
-TMP_163) in (let TMP_165 \def (THead k u0 t0) in (let TMP_166 \def (lift h d 
-TMP_165) in (let TMP_167 \def (lift_head k u0 t0 h d) in (let TMP_168 \def 
-(eq_ind_r T TMP_123 TMP_131 TMP_164 TMP_166 TMP_167) in (let TMP_169 \def 
-(THead k u0 t3) in (let TMP_170 \def (lift h d TMP_169) in (let TMP_171 \def 
-(lift_head k u0 t3 h d) in (eq_ind_r T TMP_113 TMP_119 TMP_168 TMP_170 
-TMP_171)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in (let 
-TMP_243 \def (\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i0: 
-nat).(\lambda (_: (subst0 i0 v u1 u2)).(\lambda (H1: ((\forall (d: nat).((lt 
-i0 d) \to (\forall (h: nat).(subst0 i0 (lift h (minus d (S i0)) v) (lift h d 
-u1) (lift h d u2))))))).(\lambda (k: K).(\lambda (t0: T).(\lambda (t3: 
-T).(\lambda (_: (subst0 (s k i0) v t0 t3)).(\lambda (H3: ((\forall (d: 
+(lift h d u1) (lift h d u2))))))).(\lambda (k: K).(\lambda (t0: T).(\lambda 
+(t3: T).(\lambda (_: (subst0 (s k i0) v t0 t3)).(\lambda (H3: ((\forall (d: 
 nat).((lt (s k i0) d) \to (\forall (h: nat).(subst0 (s k i0) (lift h (minus d 
 (S (s k i0))) v) (lift h d t0) (lift h d t3))))))).(\lambda (d: nat).(\lambda 
-(H4: (lt i0 d)).(\lambda (h: nat).(let TMP_173 \def (s k i0) in (let TMP_174 
-\def (S TMP_173) in (let TMP_180 \def (\lambda (n: nat).(\forall (d0: 
-nat).((lt (s k i0) d0) \to (\forall (h0: nat).(let TMP_175 \def (s k i0) in 
-(let TMP_176 \def (minus d0 n) in (let TMP_177 \def (lift h0 TMP_176 v) in 
-(let TMP_178 \def (lift h0 d0 t0) in (let TMP_179 \def (lift h0 d0 t3) in 
-(subst0 TMP_175 TMP_177 TMP_178 TMP_179)))))))))) in (let TMP_181 \def (S i0) 
-in (let TMP_182 \def (s k TMP_181) in (let TMP_183 \def (s_S k i0) in (let H5 
-\def (eq_ind_r nat TMP_174 TMP_180 H3 TMP_182 TMP_183) in (let TMP_184 \def 
-(lift h d u1) in (let TMP_185 \def (s k d) in (let TMP_186 \def (lift h 
-TMP_185 t0) in (let TMP_187 \def (THead k TMP_184 TMP_186) in (let TMP_193 
-\def (\lambda (t: T).(let TMP_188 \def (S i0) in (let TMP_189 \def (minus d 
-TMP_188) in (let TMP_190 \def (lift h TMP_189 v) in (let TMP_191 \def (THead 
-k u2 t3) in (let TMP_192 \def (lift h d TMP_191) in (subst0 i0 TMP_190 t 
-TMP_192))))))) in (let TMP_194 \def (lift h d u2) in (let TMP_195 \def (s k 
-d) in (let TMP_196 \def (lift h TMP_195 t3) in (let TMP_197 \def (THead k 
-TMP_194 TMP_196) in (let TMP_205 \def (\lambda (t: T).(let TMP_198 \def (S 
-i0) in (let TMP_199 \def (minus d TMP_198) in (let TMP_200 \def (lift h 
-TMP_199 v) in (let TMP_201 \def (lift h d u1) in (let TMP_202 \def (s k d) in 
-(let TMP_203 \def (lift h TMP_202 t0) in (let TMP_204 \def (THead k TMP_201 
-TMP_203) in (subst0 i0 TMP_200 TMP_204 t))))))))) in (let TMP_206 \def (S i0) 
-in (let TMP_207 \def (minus d TMP_206) in (let TMP_208 \def (lift h TMP_207 
-v) in (let TMP_209 \def (lift h d u1) in (let TMP_210 \def (lift h d u2) in 
-(let TMP_211 \def (H1 d H4 h) in (let TMP_212 \def (s k d) in (let TMP_213 
-\def (lift h TMP_212 t0) in (let TMP_214 \def (s k d) in (let TMP_215 \def 
-(lift h TMP_214 t3) in (let TMP_216 \def (s k d) in (let TMP_217 \def (S i0) 
-in (let TMP_218 \def (s k TMP_217) in (let TMP_219 \def (minus TMP_216 
-TMP_218) in (let TMP_226 \def (\lambda (n: nat).(let TMP_220 \def (s k i0) in 
-(let TMP_221 \def (lift h n v) in (let TMP_222 \def (s k d) in (let TMP_223 
-\def (lift h TMP_222 t0) in (let TMP_224 \def (s k d) in (let TMP_225 \def 
-(lift h TMP_224 t3) in (subst0 TMP_220 TMP_221 TMP_223 TMP_225)))))))) in 
-(let TMP_227 \def (s k d) in (let TMP_228 \def (s_lt k i0 d H4) in (let 
-TMP_229 \def (H5 TMP_227 TMP_228 h) in (let TMP_230 \def (S i0) in (let 
-TMP_231 \def (minus d TMP_230) in (let TMP_232 \def (S i0) in (let TMP_233 
-\def (minus_s_s k d TMP_232) in (let TMP_234 \def (eq_ind nat TMP_219 TMP_226 
-TMP_229 TMP_231 TMP_233) in (let TMP_235 \def (subst0_both TMP_208 TMP_209 
-TMP_210 i0 TMP_211 k TMP_213 TMP_215 TMP_234) in (let TMP_236 \def (THead k 
-u2 t3) in (let TMP_237 \def (lift h d TMP_236) in (let TMP_238 \def 
-(lift_head k u2 t3 h d) in (let TMP_239 \def (eq_ind_r T TMP_197 TMP_205 
-TMP_235 TMP_237 TMP_238) in (let TMP_240 \def (THead k u1 t0) in (let TMP_241 
-\def (lift h d TMP_240) in (let TMP_242 \def (lift_head k u1 t0 h d) in 
-(eq_ind_r T TMP_187 TMP_193 TMP_239 TMP_241 
-TMP_242))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in 
-(subst0_ind TMP_6 TMP_59 TMP_98 TMP_172 TMP_243 i u t1 t2 H)))))))))).
+(H4: (lt i0 d)).(\lambda (h: nat).(let H5 \def (eq_ind_r nat (S (s k i0)) 
+(\lambda (n: nat).(\forall (d0: nat).((lt (s k i0) d0) \to (\forall (h0: 
+nat).(subst0 (s k i0) (lift h0 (minus d0 n) v) (lift h0 d0 t0) (lift h0 d0 
+t3)))))) H3 (s k (S i0)) (s_S k i0)) in (eq_ind_r T (THead k (lift h d u1) 
+(lift h (s k d) t0)) (\lambda (t: T).(subst0 i0 (lift h (minus d (S i0)) v) t 
+(lift h d (THead k u2 t3)))) (eq_ind_r T (THead k (lift h d u2) (lift h (s k 
+d) t3)) (\lambda (t: T).(subst0 i0 (lift h (minus d (S i0)) v) (THead k (lift 
+h d u1) (lift h (s k d) t0)) t)) (subst0_both (lift h (minus d (S i0)) v) 
+(lift h d u1) (lift h d u2) i0 (H1 d H4 h) k (lift h (s k d) t0) (lift h (s k 
+d) t3) (eq_ind nat (minus (s k d) (s k (S i0))) (\lambda (n: nat).(subst0 (s 
+k i0) (lift h n v) (lift h (s k d) t0) (lift h (s k d) t3))) (H5 (s k d) 
+(s_lt k i0 d H4) h) (minus d (S i0)) (minus_s_s k d (S i0)))) (lift h d 
+(THead k u2 t3)) (lift_head k u2 t3 h d)) (lift h d (THead k u1 t0)) 
+(lift_head k u1 t0 h d))))))))))))))))) i u t1 t2 H))))).
 
-theorem subst0_lift_ge:
+lemma subst0_lift_ge:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).(\forall 
 (h: nat).((subst0 i u t1 t2) \to (\forall (d: nat).((le d i) \to (subst0 
 (plus i h) u (lift h d t1) (lift h d t2)))))))))
 \def
  \lambda (t1: T).(\lambda (t2: T).(\lambda (u: T).(\lambda (i: nat).(\lambda 
-(h: nat).(\lambda (H: (subst0 i u t1 t2)).(let TMP_4 \def (\lambda (n: 
+(h: nat).(\lambda (H: (subst0 i u t1 t2)).(subst0_ind (\lambda (n: 
 nat).(\lambda (t: T).(\lambda (t0: T).(\lambda (t3: T).(\forall (d: nat).((le 
-d n) \to (let TMP_1 \def (plus n h) in (let TMP_2 \def (lift h d t0) in (let 
-TMP_3 \def (lift h d t3) in (subst0 TMP_1 t TMP_2 TMP_3)))))))))) in (let 
-TMP_52 \def (\lambda (v: T).(\lambda (i0: nat).(\lambda (d: nat).(\lambda 
-(H0: (le d i0)).(let TMP_5 \def (plus i0 h) in (let TMP_6 \def (TLRef TMP_5) 
-in (let TMP_11 \def (\lambda (t: T).(let TMP_7 \def (plus i0 h) in (let TMP_8 
-\def (S i0) in (let TMP_9 \def (lift TMP_8 O v) in (let TMP_10 \def (lift h d 
-TMP_9) in (subst0 TMP_7 v t TMP_10)))))) in (let TMP_12 \def (S i0) in (let 
-TMP_13 \def (plus h TMP_12) in (let TMP_14 \def (lift TMP_13 O v) in (let 
-TMP_18 \def (\lambda (t: T).(let TMP_15 \def (plus i0 h) in (let TMP_16 \def 
-(plus i0 h) in (let TMP_17 \def (TLRef TMP_16) in (subst0 TMP_15 v TMP_17 
-t))))) in (let TMP_19 \def (plus h i0) in (let TMP_20 \def (S TMP_19) in (let 
-TMP_25 \def (\lambda (n: nat).(let TMP_21 \def (plus i0 h) in (let TMP_22 
-\def (plus i0 h) in (let TMP_23 \def (TLRef TMP_22) in (let TMP_24 \def (lift 
-n O v) in (subst0 TMP_21 v TMP_23 TMP_24)))))) in (let TMP_26 \def (plus h 
-i0) in (let TMP_31 \def (\lambda (n: nat).(let TMP_27 \def (TLRef n) in (let 
-TMP_28 \def (plus h i0) in (let TMP_29 \def (S TMP_28) in (let TMP_30 \def 
-(lift TMP_29 O v) in (subst0 n v TMP_27 TMP_30)))))) in (let TMP_32 \def 
-(plus h i0) in (let TMP_33 \def (subst0_lref v TMP_32) in (let TMP_34 \def 
-(plus i0 h) in (let TMP_35 \def (plus_sym i0 h) in (let TMP_36 \def (eq_ind_r 
-nat TMP_26 TMP_31 TMP_33 TMP_34 TMP_35) in (let TMP_37 \def (S i0) in (let 
-TMP_38 \def (plus h TMP_37) in (let TMP_39 \def (plus_n_Sm h i0) in (let 
-TMP_40 \def (eq_ind nat TMP_20 TMP_25 TMP_36 TMP_38 TMP_39) in (let TMP_41 
-\def (S i0) in (let TMP_42 \def (lift TMP_41 O v) in (let TMP_43 \def (lift h 
-d TMP_42) in (let TMP_44 \def (S i0) in (let TMP_45 \def (le_S d i0 H0) in 
-(let TMP_46 \def (le_O_n d) in (let TMP_47 \def (lift_free v TMP_44 h O d 
-TMP_45 TMP_46) in (let TMP_48 \def (eq_ind_r T TMP_14 TMP_18 TMP_40 TMP_43 
-TMP_47) in (let TMP_49 \def (TLRef i0) in (let TMP_50 \def (lift h d TMP_49) 
-in (let TMP_51 \def (lift_lref_ge i0 h d H0) in (eq_ind_r T TMP_6 TMP_11 
-TMP_48 TMP_50 TMP_51))))))))))))))))))))))))))))))))))))) in (let TMP_85 \def 
-(\lambda (v: T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i0: nat).(\lambda 
-(_: (subst0 i0 v u1 u2)).(\lambda (H1: ((\forall (d: nat).((le d i0) \to 
-(subst0 (plus i0 h) v (lift h d u1) (lift h d u2)))))).(\lambda (t: 
-T).(\lambda (k: K).(\lambda (d: nat).(\lambda (H2: (le d i0)).(let TMP_53 
-\def (lift h d u1) in (let TMP_54 \def (s k d) in (let TMP_55 \def (lift h 
-TMP_54 t) in (let TMP_56 \def (THead k TMP_53 TMP_55) in (let TMP_60 \def 
-(\lambda (t0: T).(let TMP_57 \def (plus i0 h) in (let TMP_58 \def (THead k u2 
-t) in (let TMP_59 \def (lift h d TMP_58) in (subst0 TMP_57 v t0 TMP_59))))) 
-in (let TMP_61 \def (lift h d u2) in (let TMP_62 \def (s k d) in (let TMP_63 
-\def (lift h TMP_62 t) in (let TMP_64 \def (THead k TMP_61 TMP_63) in (let 
-TMP_70 \def (\lambda (t0: T).(let TMP_65 \def (plus i0 h) in (let TMP_66 \def 
-(lift h d u1) in (let TMP_67 \def (s k d) in (let TMP_68 \def (lift h TMP_67 
-t) in (let TMP_69 \def (THead k TMP_66 TMP_68) in (subst0 TMP_65 v TMP_69 
-t0))))))) in (let TMP_71 \def (lift h d u2) in (let TMP_72 \def (lift h d u1) 
-in (let TMP_73 \def (plus i0 h) in (let TMP_74 \def (H1 d H2) in (let TMP_75 
-\def (s k d) in (let TMP_76 \def (lift h TMP_75 t) in (let TMP_77 \def 
-(subst0_fst v TMP_71 TMP_72 TMP_73 TMP_74 TMP_76 k) in (let TMP_78 \def 
-(THead k u2 t) in (let TMP_79 \def (lift h d TMP_78) in (let TMP_80 \def 
-(lift_head k u2 t h d) in (let TMP_81 \def (eq_ind_r T TMP_64 TMP_70 TMP_77 
-TMP_79 TMP_80) in (let TMP_82 \def (THead k u1 t) in (let TMP_83 \def (lift h 
-d TMP_82) in (let TMP_84 \def (lift_head k u1 t h d) in (eq_ind_r T TMP_56 
-TMP_60 TMP_81 TMP_83 TMP_84))))))))))))))))))))))))))))))))))) in (let 
-TMP_129 \def (\lambda (k: K).(\lambda (v: T).(\lambda (t0: T).(\lambda (t3: 
-T).(\lambda (i0: nat).(\lambda (_: (subst0 (s k i0) v t3 t0)).(\lambda (H1: 
-((\forall (d: nat).((le d (s k i0)) \to (subst0 (plus (s k i0) h) v (lift h d 
-t3) (lift h d t0)))))).(\lambda (u0: T).(\lambda (d: nat).(\lambda (H2: (le d 
-i0)).(let TMP_86 \def (s k i0) in (let TMP_87 \def (plus TMP_86 h) in (let 
-TMP_90 \def (\lambda (n: nat).(\forall (d0: nat).((le d0 (s k i0)) \to (let 
-TMP_88 \def (lift h d0 t3) in (let TMP_89 \def (lift h d0 t0) in (subst0 n v 
-TMP_88 TMP_89)))))) in (let TMP_91 \def (plus i0 h) in (let TMP_92 \def (s k 
-TMP_91) in (let TMP_93 \def (s_plus k i0 h) in (let H3 \def (eq_ind_r nat 
-TMP_87 TMP_90 H1 TMP_92 TMP_93) in (let TMP_94 \def (lift h d u0) in (let 
-TMP_95 \def (s k d) in (let TMP_96 \def (lift h TMP_95 t3) in (let TMP_97 
-\def (THead k TMP_94 TMP_96) in (let TMP_101 \def (\lambda (t: T).(let TMP_98 
-\def (plus i0 h) in (let TMP_99 \def (THead k u0 t0) in (let TMP_100 \def 
-(lift h d TMP_99) in (subst0 TMP_98 v t TMP_100))))) in (let TMP_102 \def 
-(lift h d u0) in (let TMP_103 \def (s k d) in (let TMP_104 \def (lift h 
-TMP_103 t0) in (let TMP_105 \def (THead k TMP_102 TMP_104) in (let TMP_111 
-\def (\lambda (t: T).(let TMP_106 \def (plus i0 h) in (let TMP_107 \def (lift 
-h d u0) in (let TMP_108 \def (s k d) in (let TMP_109 \def (lift h TMP_108 t3) 
-in (let TMP_110 \def (THead k TMP_107 TMP_109) in (subst0 TMP_106 v TMP_110 
-t))))))) in (let TMP_112 \def (s k d) in (let TMP_113 \def (lift h TMP_112 
-t0) in (let TMP_114 \def (s k d) in (let TMP_115 \def (lift h TMP_114 t3) in 
-(let TMP_116 \def (plus i0 h) in (let TMP_117 \def (s k d) in (let TMP_118 
-\def (s_le k d i0 H2) in (let TMP_119 \def (H3 TMP_117 TMP_118) in (let 
-TMP_120 \def (lift h d u0) in (let TMP_121 \def (subst0_snd k v TMP_113 
-TMP_115 TMP_116 TMP_119 TMP_120) in (let TMP_122 \def (THead k u0 t0) in (let 
-TMP_123 \def (lift h d TMP_122) in (let TMP_124 \def (lift_head k u0 t0 h d) 
-in (let TMP_125 \def (eq_ind_r T TMP_105 TMP_111 TMP_121 TMP_123 TMP_124) in 
-(let TMP_126 \def (THead k u0 t3) in (let TMP_127 \def (lift h d TMP_126) in 
-(let TMP_128 \def (lift_head k u0 t3 h d) in (eq_ind_r T TMP_97 TMP_101 
-TMP_125 TMP_127 TMP_128))))))))))))))))))))))))))))))))))))))))))))) in (let 
-TMP_175 \def (\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i0: 
+d n) \to (subst0 (plus n h) t (lift h d t0) (lift h d t3)))))))) (\lambda (v: 
+T).(\lambda (i0: nat).(\lambda (d: nat).(\lambda (H0: (le d i0)).(eq_ind_r T 
+(TLRef (plus i0 h)) (\lambda (t: T).(subst0 (plus i0 h) v t (lift h d (lift 
+(S i0) O v)))) (eq_ind_r T (lift (plus h (S i0)) O v) (\lambda (t: T).(subst0 
+(plus i0 h) v (TLRef (plus i0 h)) t)) (eq_ind nat (S (plus h i0)) (\lambda 
+(n: nat).(subst0 (plus i0 h) v (TLRef (plus i0 h)) (lift n O v))) (eq_ind_r 
+nat (plus h i0) (\lambda (n: nat).(subst0 n v (TLRef n) (lift (S (plus h i0)) 
+O v))) (subst0_lref v (plus h i0)) (plus i0 h) (plus_sym i0 h)) (plus h (S 
+i0)) (plus_n_Sm h i0)) (lift h d (lift (S i0) O v)) (lift_free v (S i0) h O d 
+(le_S d i0 H0) (le_O_n d))) (lift h d (TLRef i0)) (lift_lref_ge i0 h d 
+H0)))))) (\lambda (v: T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i0: 
 nat).(\lambda (_: (subst0 i0 v u1 u2)).(\lambda (H1: ((\forall (d: nat).((le 
-d i0) \to (subst0 (plus i0 h) v (lift h d u1) (lift h d u2)))))).(\lambda (k: 
+d i0) \to (subst0 (plus i0 h) v (lift h d u1) (lift h d u2)))))).(\lambda (t: 
+T).(\lambda (k: K).(\lambda (d: nat).(\lambda (H2: (le d i0)).(eq_ind_r T 
+(THead k (lift h d u1) (lift h (s k d) t)) (\lambda (t0: T).(subst0 (plus i0 
+h) v t0 (lift h d (THead k u2 t)))) (eq_ind_r T (THead k (lift h d u2) (lift 
+h (s k d) t)) (\lambda (t0: T).(subst0 (plus i0 h) v (THead k (lift h d u1) 
+(lift h (s k d) t)) t0)) (subst0_fst v (lift h d u2) (lift h d u1) (plus i0 
+h) (H1 d H2) (lift h (s k d) t) k) (lift h d (THead k u2 t)) (lift_head k u2 
+t h d)) (lift h d (THead k u1 t)) (lift_head k u1 t h d)))))))))))) (\lambda 
+(k: K).(\lambda (v: T).(\lambda (t0: T).(\lambda (t3: T).(\lambda (i0: 
+nat).(\lambda (_: (subst0 (s k i0) v t3 t0)).(\lambda (H1: ((\forall (d: 
+nat).((le d (s k i0)) \to (subst0 (plus (s k i0) h) v (lift h d t3) (lift h d 
+t0)))))).(\lambda (u0: T).(\lambda (d: nat).(\lambda (H2: (le d i0)).(let H3 
+\def (eq_ind_r nat (plus (s k i0) h) (\lambda (n: nat).(\forall (d0: 
+nat).((le d0 (s k i0)) \to (subst0 n v (lift h d0 t3) (lift h d0 t0))))) H1 
+(s k (plus i0 h)) (s_plus k i0 h)) in (eq_ind_r T (THead k (lift h d u0) 
+(lift h (s k d) t3)) (\lambda (t: T).(subst0 (plus i0 h) v t (lift h d (THead 
+k u0 t0)))) (eq_ind_r T (THead k (lift h d u0) (lift h (s k d) t0)) (\lambda 
+(t: T).(subst0 (plus i0 h) v (THead k (lift h d u0) (lift h (s k d) t3)) t)) 
+(subst0_snd k v (lift h (s k d) t0) (lift h (s k d) t3) (plus i0 h) (H3 (s k 
+d) (s_le k d i0 H2)) (lift h d u0)) (lift h d (THead k u0 t0)) (lift_head k 
+u0 t0 h d)) (lift h d (THead k u0 t3)) (lift_head k u0 t3 h d))))))))))))) 
+(\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i0: nat).(\lambda 
+(_: (subst0 i0 v u1 u2)).(\lambda (H1: ((\forall (d: nat).((le d i0) \to 
+(subst0 (plus i0 h) v (lift h d u1) (lift h d u2)))))).(\lambda (k: 
 K).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (subst0 (s k i0) v t0 
 t3)).(\lambda (H3: ((\forall (d: nat).((le d (s k i0)) \to (subst0 (plus (s k 
 i0) h) v (lift h d t0) (lift h d t3)))))).(\lambda (d: nat).(\lambda (H4: (le 
-d i0)).(let TMP_130 \def (s k i0) in (let TMP_131 \def (plus TMP_130 h) in 
-(let TMP_134 \def (\lambda (n: nat).(\forall (d0: nat).((le d0 (s k i0)) \to 
-(let TMP_132 \def (lift h d0 t0) in (let TMP_133 \def (lift h d0 t3) in 
-(subst0 n v TMP_132 TMP_133)))))) in (let TMP_135 \def (plus i0 h) in (let 
-TMP_136 \def (s k TMP_135) in (let TMP_137 \def (s_plus k i0 h) in (let H5 
-\def (eq_ind_r nat TMP_131 TMP_134 H3 TMP_136 TMP_137) in (let TMP_138 \def 
-(lift h d u1) in (let TMP_139 \def (s k d) in (let TMP_140 \def (lift h 
-TMP_139 t0) in (let TMP_141 \def (THead k TMP_138 TMP_140) in (let TMP_145 
-\def (\lambda (t: T).(let TMP_142 \def (plus i0 h) in (let TMP_143 \def 
-(THead k u2 t3) in (let TMP_144 \def (lift h d TMP_143) in (subst0 TMP_142 v 
-t TMP_144))))) in (let TMP_146 \def (lift h d u2) in (let TMP_147 \def (s k 
-d) in (let TMP_148 \def (lift h TMP_147 t3) in (let TMP_149 \def (THead k 
-TMP_146 TMP_148) in (let TMP_155 \def (\lambda (t: T).(let TMP_150 \def (plus 
-i0 h) in (let TMP_151 \def (lift h d u1) in (let TMP_152 \def (s k d) in (let 
-TMP_153 \def (lift h TMP_152 t0) in (let TMP_154 \def (THead k TMP_151 
-TMP_153) in (subst0 TMP_150 v TMP_154 t))))))) in (let TMP_156 \def (lift h d 
-u1) in (let TMP_157 \def (lift h d u2) in (let TMP_158 \def (plus i0 h) in 
-(let TMP_159 \def (H1 d H4) in (let TMP_160 \def (s k d) in (let TMP_161 \def 
-(lift h TMP_160 t0) in (let TMP_162 \def (s k d) in (let TMP_163 \def (lift h 
-TMP_162 t3) in (let TMP_164 \def (s k d) in (let TMP_165 \def (s_le k d i0 
-H4) in (let TMP_166 \def (H5 TMP_164 TMP_165) in (let TMP_167 \def 
-(subst0_both v TMP_156 TMP_157 TMP_158 TMP_159 k TMP_161 TMP_163 TMP_166) in 
-(let TMP_168 \def (THead k u2 t3) in (let TMP_169 \def (lift h d TMP_168) in 
-(let TMP_170 \def (lift_head k u2 t3 h d) in (let TMP_171 \def (eq_ind_r T 
-TMP_149 TMP_155 TMP_167 TMP_169 TMP_170) in (let TMP_172 \def (THead k u1 t0) 
-in (let TMP_173 \def (lift h d TMP_172) in (let TMP_174 \def (lift_head k u1 
-t0 h d) in (eq_ind_r T TMP_141 TMP_145 TMP_171 TMP_173 
-TMP_174)))))))))))))))))))))))))))))))))))))))))))))))))) in (subst0_ind 
-TMP_4 TMP_52 TMP_85 TMP_129 TMP_175 i u t1 t2 H))))))))))).
+d i0)).(let H5 \def (eq_ind_r nat (plus (s k i0) h) (\lambda (n: 
+nat).(\forall (d0: nat).((le d0 (s k i0)) \to (subst0 n v (lift h d0 t0) 
+(lift h d0 t3))))) H3 (s k (plus i0 h)) (s_plus k i0 h)) in (eq_ind_r T 
+(THead k (lift h d u1) (lift h (s k d) t0)) (\lambda (t: T).(subst0 (plus i0 
+h) v t (lift h d (THead k u2 t3)))) (eq_ind_r T (THead k (lift h d u2) (lift 
+h (s k d) t3)) (\lambda (t: T).(subst0 (plus i0 h) v (THead k (lift h d u1) 
+(lift h (s k d) t0)) t)) (subst0_both v (lift h d u1) (lift h d u2) (plus i0 
+h) (H1 d H4) k (lift h (s k d) t0) (lift h (s k d) t3) (H5 (s k d) (s_le k d 
+i0 H4))) (lift h d (THead k u2 t3)) (lift_head k u2 t3 h d)) (lift h d (THead 
+k u1 t0)) (lift_head k u1 t0 h d)))))))))))))))) i u t1 t2 H)))))).
 
-theorem subst0_lift_ge_S:
+lemma subst0_lift_ge_S:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst0 
 i u t1 t2) \to (\forall (d: nat).((le d i) \to (subst0 (S i) u (lift (S O) d 
 t1) (lift (S O) d t2))))))))
 \def
  \lambda (t1: T).(\lambda (t2: T).(\lambda (u: T).(\lambda (i: nat).(\lambda 
-(H: (subst0 i u t1 t2)).(\lambda (d: nat).(\lambda (H0: (le d i)).(let TMP_1 
-\def (S O) in (let TMP_2 \def (plus i TMP_1) in (let TMP_7 \def (\lambda (n: 
-nat).(let TMP_3 \def (S O) in (let TMP_4 \def (lift TMP_3 d t1) in (let TMP_5 
-\def (S O) in (let TMP_6 \def (lift TMP_5 d t2) in (subst0 n u TMP_4 
-TMP_6)))))) in (let TMP_8 \def (S O) in (let TMP_9 \def (subst0_lift_ge t1 t2 
-u i TMP_8 H d H0) in (let TMP_10 \def (S i) in (let TMP_11 \def (S O) in (let 
-TMP_12 \def (plus TMP_11 i) in (let TMP_14 \def (\lambda (n: nat).(let TMP_13 
-\def (S i) in (eq nat n TMP_13))) in (let TMP_15 \def (S O) in (let TMP_16 
-\def (plus TMP_15 i) in (let TMP_17 \def (S i) in (let TMP_18 \def (S i) in 
-(let TMP_19 \def (le_n TMP_18) in (let TMP_20 \def (S O) in (let TMP_21 \def 
-(plus TMP_20 i) in (let TMP_22 \def (le_n TMP_21) in (let TMP_23 \def 
-(le_antisym TMP_16 TMP_17 TMP_19 TMP_22) in (let TMP_24 \def (S O) in (let 
-TMP_25 \def (plus i TMP_24) in (let TMP_26 \def (S O) in (let TMP_27 \def 
-(plus_sym i TMP_26) in (let TMP_28 \def (eq_ind_r nat TMP_12 TMP_14 TMP_23 
-TMP_25 TMP_27) in (eq_ind nat TMP_2 TMP_7 TMP_9 TMP_10 
-TMP_28)))))))))))))))))))))))))))))).
+(H: (subst0 i u t1 t2)).(\lambda (d: nat).(\lambda (H0: (le d i)).(eq_ind nat 
+(plus i (S O)) (\lambda (n: nat).(subst0 n u (lift (S O) d t1) (lift (S O) d 
+t2))) (subst0_lift_ge t1 t2 u i (S O) H d H0) (S i) (eq_ind_r nat (plus (S O) 
+i) (\lambda (n: nat).(eq nat n (S i))) (le_antisym (plus (S O) i) (S i) (le_n 
+(S i)) (le_n (plus (S O) i))) (plus i (S O)) (plus_sym i (S O)))))))))).
 
-theorem subst0_lift_ge_s:
+lemma subst0_lift_ge_s:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst0 
 i u t1 t2) \to (\forall (d: nat).((le d i) \to (\forall (b: B).(subst0 (s 
 (Bind b) i) u (lift (S O) d t1) (lift (S O) d t2)))))))))