- \lambda (t: T).(let TMP_6 \def (\lambda (t0: T).(\forall (h: nat).(\forall
-(k: nat).(\forall (d: nat).(\forall (e: nat).((le e d) \to (let TMP_1 \def
-(plus k d) in (let TMP_2 \def (lift k e t0) in (let TMP_3 \def (lift h TMP_1
-TMP_2) in (let TMP_4 \def (lift h d t0) in (let TMP_5 \def (lift k e TMP_4)
-in (eq T TMP_3 TMP_5)))))))))))) in (let TMP_45 \def (\lambda (n:
-nat).(\lambda (h: nat).(\lambda (k: nat).(\lambda (d: nat).(\lambda (e:
-nat).(\lambda (_: (le e d)).(let TMP_7 \def (TSort n) in (let TMP_13 \def
-(\lambda (t0: T).(let TMP_8 \def (plus k d) in (let TMP_9 \def (lift h TMP_8
-t0) in (let TMP_10 \def (TSort n) in (let TMP_11 \def (lift h d TMP_10) in
-(let TMP_12 \def (lift k e TMP_11) in (eq T TMP_9 TMP_12))))))) in (let
-TMP_14 \def (TSort n) in (let TMP_18 \def (\lambda (t0: T).(let TMP_15 \def
-(TSort n) in (let TMP_16 \def (lift h d TMP_15) in (let TMP_17 \def (lift k e
-TMP_16) in (eq T t0 TMP_17))))) in (let TMP_19 \def (TSort n) in (let TMP_22
-\def (\lambda (t0: T).(let TMP_20 \def (TSort n) in (let TMP_21 \def (lift k
-e t0) in (eq T TMP_20 TMP_21)))) in (let TMP_23 \def (TSort n) in (let TMP_25
-\def (\lambda (t0: T).(let TMP_24 \def (TSort n) in (eq T TMP_24 t0))) in
-(let TMP_26 \def (TSort n) in (let TMP_27 \def (refl_equal T TMP_26) in (let
-TMP_28 \def (TSort n) in (let TMP_29 \def (lift k e TMP_28) in (let TMP_30
-\def (lift_sort n k e) in (let TMP_31 \def (eq_ind_r T TMP_23 TMP_25 TMP_27
-TMP_29 TMP_30) in (let TMP_32 \def (TSort n) in (let TMP_33 \def (lift h d
-TMP_32) in (let TMP_34 \def (lift_sort n h d) in (let TMP_35 \def (eq_ind_r T
-TMP_19 TMP_22 TMP_31 TMP_33 TMP_34) in (let TMP_36 \def (plus k d) in (let
-TMP_37 \def (TSort n) in (let TMP_38 \def (lift h TMP_36 TMP_37) in (let
-TMP_39 \def (plus k d) in (let TMP_40 \def (lift_sort n h TMP_39) in (let
-TMP_41 \def (eq_ind_r T TMP_14 TMP_18 TMP_35 TMP_38 TMP_40) in (let TMP_42
-\def (TSort n) in (let TMP_43 \def (lift k e TMP_42) in (let TMP_44 \def
-(lift_sort n k e) in (eq_ind_r T TMP_7 TMP_13 TMP_41 TMP_43
-TMP_44)))))))))))))))))))))))))))))))))) in (let TMP_212 \def (\lambda (n:
-nat).(\lambda (h: nat).(\lambda (k: nat).(\lambda (d: nat).(\lambda (e:
-nat).(\lambda (H: (le e d)).(let TMP_46 \def (plus k d) in (let TMP_47 \def
-(TLRef n) in (let TMP_48 \def (lift k e TMP_47) in (let TMP_49 \def (lift h
-TMP_46 TMP_48) in (let TMP_50 \def (TLRef n) in (let TMP_51 \def (lift h d
-TMP_50) in (let TMP_52 \def (lift k e TMP_51) in (let TMP_53 \def (eq T
-TMP_49 TMP_52) in (let TMP_95 \def (\lambda (H0: (lt n e)).(let H1 \def
-(lt_le_trans n e d H0 H) in (let TMP_54 \def (TLRef n) in (let TMP_60 \def
-(\lambda (t0: T).(let TMP_55 \def (plus k d) in (let TMP_56 \def (lift h
-TMP_55 t0) in (let TMP_57 \def (TLRef n) in (let TMP_58 \def (lift h d
-TMP_57) in (let TMP_59 \def (lift k e TMP_58) in (eq T TMP_56 TMP_59)))))))
-in (let TMP_61 \def (TLRef n) in (let TMP_65 \def (\lambda (t0: T).(let
-TMP_62 \def (TLRef n) in (let TMP_63 \def (lift h d TMP_62) in (let TMP_64
-\def (lift k e TMP_63) in (eq T t0 TMP_64))))) in (let TMP_66 \def (TLRef n)
-in (let TMP_69 \def (\lambda (t0: T).(let TMP_67 \def (TLRef n) in (let
-TMP_68 \def (lift k e t0) in (eq T TMP_67 TMP_68)))) in (let TMP_70 \def
-(TLRef n) in (let TMP_72 \def (\lambda (t0: T).(let TMP_71 \def (TLRef n) in
-(eq T TMP_71 t0))) in (let TMP_73 \def (TLRef n) in (let TMP_74 \def
-(refl_equal T TMP_73) in (let TMP_75 \def (TLRef n) in (let TMP_76 \def (lift
-k e TMP_75) in (let TMP_77 \def (lift_lref_lt n k e H0) in (let TMP_78 \def
-(eq_ind_r T TMP_70 TMP_72 TMP_74 TMP_76 TMP_77) in (let TMP_79 \def (TLRef n)
-in (let TMP_80 \def (lift h d TMP_79) in (let TMP_81 \def (lift_lref_lt n h d
-H1) in (let TMP_82 \def (eq_ind_r T TMP_66 TMP_69 TMP_78 TMP_80 TMP_81) in
-(let TMP_83 \def (plus k d) in (let TMP_84 \def (TLRef n) in (let TMP_85 \def
-(lift h TMP_83 TMP_84) in (let TMP_86 \def (plus k d) in (let TMP_87 \def
-(plus k d) in (let TMP_88 \def (le_plus_r k d) in (let TMP_89 \def
-(lt_le_trans n d TMP_87 H1 TMP_88) in (let TMP_90 \def (lift_lref_lt n h
-TMP_86 TMP_89) in (let TMP_91 \def (eq_ind_r T TMP_61 TMP_65 TMP_82 TMP_85
-TMP_90) in (let TMP_92 \def (TLRef n) in (let TMP_93 \def (lift k e TMP_92)
-in (let TMP_94 \def (lift_lref_lt n k e H0) in (eq_ind_r T TMP_54 TMP_60
-TMP_91 TMP_93 TMP_94))))))))))))))))))))))))))))))))) in (let TMP_211 \def
-(\lambda (H0: (le e n)).(let TMP_96 \def (plus n k) in (let TMP_97 \def
-(TLRef TMP_96) in (let TMP_103 \def (\lambda (t0: T).(let TMP_98 \def (plus k
-d) in (let TMP_99 \def (lift h TMP_98 t0) in (let TMP_100 \def (TLRef n) in
-(let TMP_101 \def (lift h d TMP_100) in (let TMP_102 \def (lift k e TMP_101)
-in (eq T TMP_99 TMP_102))))))) in (let TMP_104 \def (plus d k) in (let
-TMP_111 \def (\lambda (n0: nat).(let TMP_105 \def (plus n k) in (let TMP_106
-\def (TLRef TMP_105) in (let TMP_107 \def (lift h n0 TMP_106) in (let TMP_108
-\def (TLRef n) in (let TMP_109 \def (lift h d TMP_108) in (let TMP_110 \def
-(lift k e TMP_109) in (eq T TMP_107 TMP_110)))))))) in (let TMP_112 \def
-(plus d k) in (let TMP_113 \def (plus n k) in (let TMP_114 \def (TLRef
-TMP_113) in (let TMP_115 \def (lift h TMP_112 TMP_114) in (let TMP_116 \def
-(TLRef n) in (let TMP_117 \def (lift h d TMP_116) in (let TMP_118 \def (lift
-k e TMP_117) in (let TMP_119 \def (eq T TMP_115 TMP_118) in (let TMP_155 \def
-(\lambda (H1: (lt n d)).(let TMP_120 \def (plus n k) in (let TMP_121 \def
-(TLRef TMP_120) in (let TMP_125 \def (\lambda (t0: T).(let TMP_122 \def
-(TLRef n) in (let TMP_123 \def (lift h d TMP_122) in (let TMP_124 \def (lift
-k e TMP_123) in (eq T t0 TMP_124))))) in (let TMP_126 \def (TLRef n) in (let
-TMP_130 \def (\lambda (t0: T).(let TMP_127 \def (plus n k) in (let TMP_128
-\def (TLRef TMP_127) in (let TMP_129 \def (lift k e t0) in (eq T TMP_128
-TMP_129))))) in (let TMP_131 \def (plus n k) in (let TMP_132 \def (TLRef
-TMP_131) in (let TMP_135 \def (\lambda (t0: T).(let TMP_133 \def (plus n k)
-in (let TMP_134 \def (TLRef TMP_133) in (eq T TMP_134 t0)))) in (let TMP_136
-\def (plus n k) in (let TMP_137 \def (TLRef TMP_136) in (let TMP_138 \def
-(refl_equal T TMP_137) in (let TMP_139 \def (TLRef n) in (let TMP_140 \def
-(lift k e TMP_139) in (let TMP_141 \def (lift_lref_ge n k e H0) in (let
-TMP_142 \def (eq_ind_r T TMP_132 TMP_135 TMP_138 TMP_140 TMP_141) in (let
-TMP_143 \def (TLRef n) in (let TMP_144 \def (lift h d TMP_143) in (let
-TMP_145 \def (lift_lref_lt n h d H1) in (let TMP_146 \def (eq_ind_r T TMP_126
-TMP_130 TMP_142 TMP_144 TMP_145) in (let TMP_147 \def (plus d k) in (let
-TMP_148 \def (plus n k) in (let TMP_149 \def (TLRef TMP_148) in (let TMP_150
-\def (lift h TMP_147 TMP_149) in (let TMP_151 \def (plus n k) in (let TMP_152
-\def (plus d k) in (let TMP_153 \def (lt_reg_r n d k H1) in (let TMP_154 \def
-(lift_lref_lt TMP_151 h TMP_152 TMP_153) in (eq_ind_r T TMP_121 TMP_125
-TMP_146 TMP_150 TMP_154))))))))))))))))))))))))))))) in (let TMP_203 \def
-(\lambda (H1: (le d n)).(let TMP_156 \def (plus n k) in (let TMP_157 \def
-(plus TMP_156 h) in (let TMP_158 \def (TLRef TMP_157) in (let TMP_162 \def
-(\lambda (t0: T).(let TMP_159 \def (TLRef n) in (let TMP_160 \def (lift h d
-TMP_159) in (let TMP_161 \def (lift k e TMP_160) in (eq T t0 TMP_161))))) in
-(let TMP_163 \def (plus n h) in (let TMP_164 \def (TLRef TMP_163) in (let
-TMP_169 \def (\lambda (t0: T).(let TMP_165 \def (plus n k) in (let TMP_166
-\def (plus TMP_165 h) in (let TMP_167 \def (TLRef TMP_166) in (let TMP_168
-\def (lift k e t0) in (eq T TMP_167 TMP_168)))))) in (let TMP_170 \def (plus
-n h) in (let TMP_171 \def (plus TMP_170 k) in (let TMP_172 \def (TLRef
-TMP_171) in (let TMP_176 \def (\lambda (t0: T).(let TMP_173 \def (plus n k)
-in (let TMP_174 \def (plus TMP_173 h) in (let TMP_175 \def (TLRef TMP_174) in
-(eq T TMP_175 t0))))) in (let TMP_177 \def (plus n k) in (let TMP_178 \def
-(plus TMP_177 h) in (let TMP_179 \def (plus n h) in (let TMP_180 \def (plus
-TMP_179 k) in (let TMP_181 \def (plus_permute_2_in_3 n k h) in (let TMP_182
-\def (f_equal nat T TLRef TMP_178 TMP_180 TMP_181) in (let TMP_183 \def (plus
-n h) in (let TMP_184 \def (TLRef TMP_183) in (let TMP_185 \def (lift k e
-TMP_184) in (let TMP_186 \def (plus n h) in (let TMP_187 \def (le_plus_trans
-e n h H0) in (let TMP_188 \def (lift_lref_ge TMP_186 k e TMP_187) in (let
-TMP_189 \def (eq_ind_r T TMP_172 TMP_176 TMP_182 TMP_185 TMP_188) in (let
-TMP_190 \def (TLRef n) in (let TMP_191 \def (lift h d TMP_190) in (let
-TMP_192 \def (lift_lref_ge n h d H1) in (let TMP_193 \def (eq_ind_r T TMP_164
-TMP_169 TMP_189 TMP_191 TMP_192) in (let TMP_194 \def (plus d k) in (let
-TMP_195 \def (plus n k) in (let TMP_196 \def (TLRef TMP_195) in (let TMP_197
-\def (lift h TMP_194 TMP_196) in (let TMP_198 \def (plus n k) in (let TMP_199
-\def (plus d k) in (let TMP_200 \def (le_n k) in (let TMP_201 \def
-(le_plus_plus d n k k H1 TMP_200) in (let TMP_202 \def (lift_lref_ge TMP_198
-h TMP_199 TMP_201) in (eq_ind_r T TMP_158 TMP_162 TMP_193 TMP_197
-TMP_202))))))))))))))))))))))))))))))))))))))) in (let TMP_204 \def (lt_le_e
-n d TMP_119 TMP_155 TMP_203) in (let TMP_205 \def (plus k d) in (let TMP_206
-\def (plus_sym k d) in (let TMP_207 \def (eq_ind_r nat TMP_104 TMP_111
-TMP_204 TMP_205 TMP_206) in (let TMP_208 \def (TLRef n) in (let TMP_209 \def
-(lift k e TMP_208) in (let TMP_210 \def (lift_lref_ge n k e H0) in (eq_ind_r
-T TMP_97 TMP_103 TMP_207 TMP_209 TMP_210)))))))))))))))))))))))) in (lt_le_e
-n e TMP_53 TMP_95 TMP_211))))))))))))))))) in (let TMP_339 \def (\lambda (k:
+ \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (h: nat).(\forall (k:
+nat).(\forall (d: nat).(\forall (e: nat).((le e d) \to (eq T (lift h (plus k
+d) (lift k e t0)) (lift k e (lift h d t0))))))))) (\lambda (n: nat).(\lambda
+(h: nat).(\lambda (k: nat).(\lambda (d: nat).(\lambda (e: nat).(\lambda (_:
+(le e d)).(eq_ind_r T (TSort n) (\lambda (t0: T).(eq T (lift h (plus k d) t0)
+(lift k e (lift h d (TSort n))))) (eq_ind_r T (TSort n) (\lambda (t0: T).(eq
+T t0 (lift k e (lift h d (TSort n))))) (eq_ind_r T (TSort n) (\lambda (t0:
+T).(eq T (TSort n) (lift k e t0))) (eq_ind_r T (TSort n) (\lambda (t0: T).(eq
+T (TSort n) t0)) (refl_equal T (TSort n)) (lift k e (TSort n)) (lift_sort n k
+e)) (lift h d (TSort n)) (lift_sort n h d)) (lift h (plus k d) (TSort n))
+(lift_sort n h (plus k d))) (lift k e (TSort n)) (lift_sort n k e))))))))
+(\lambda (n: nat).(\lambda (h: nat).(\lambda (k: nat).(\lambda (d:
+nat).(\lambda (e: nat).(\lambda (H: (le e d)).(lt_le_e n e (eq T (lift h
+(plus k d) (lift k e (TLRef n))) (lift k e (lift h d (TLRef n)))) (\lambda
+(H0: (lt n e)).(let H1 \def (lt_le_trans n e d H0 H) in (eq_ind_r T (TLRef n)
+(\lambda (t0: T).(eq T (lift h (plus k d) t0) (lift k e (lift h d (TLRef
+n))))) (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T t0 (lift k e (lift h d
+(TLRef n))))) (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T (TLRef n) (lift k
+e t0))) (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T (TLRef n) t0))
+(refl_equal T (TLRef n)) (lift k e (TLRef n)) (lift_lref_lt n k e H0)) (lift
+h d (TLRef n)) (lift_lref_lt n h d H1)) (lift h (plus k d) (TLRef n))
+(lift_lref_lt n h (plus k d) (lt_le_trans n d (plus k d) H1 (le_plus_r k
+d)))) (lift k e (TLRef n)) (lift_lref_lt n k e H0)))) (\lambda (H0: (le e
+n)).(eq_ind_r T (TLRef (plus n k)) (\lambda (t0: T).(eq T (lift h (plus k d)
+t0) (lift k e (lift h d (TLRef n))))) (eq_ind_r nat (plus d k) (\lambda (n0:
+nat).(eq T (lift h n0 (TLRef (plus n k))) (lift k e (lift h d (TLRef n)))))
+(lt_le_e n d (eq T (lift h (plus d k) (TLRef (plus n k))) (lift k e (lift h d
+(TLRef n)))) (\lambda (H1: (lt n d)).(eq_ind_r T (TLRef (plus n k)) (\lambda
+(t0: T).(eq T t0 (lift k e (lift h d (TLRef n))))) (eq_ind_r T (TLRef n)
+(\lambda (t0: T).(eq T (TLRef (plus n k)) (lift k e t0))) (eq_ind_r T (TLRef
+(plus n k)) (\lambda (t0: T).(eq T (TLRef (plus n k)) t0)) (refl_equal T
+(TLRef (plus n k))) (lift k e (TLRef n)) (lift_lref_ge n k e H0)) (lift h d
+(TLRef n)) (lift_lref_lt n h d H1)) (lift h (plus d k) (TLRef (plus n k)))
+(lift_lref_lt (plus n k) h (plus d k) (lt_reg_r n d k H1)))) (\lambda (H1:
+(le d n)).(eq_ind_r T (TLRef (plus (plus n k) h)) (\lambda (t0: T).(eq T t0
+(lift k e (lift h d (TLRef n))))) (eq_ind_r T (TLRef (plus n h)) (\lambda
+(t0: T).(eq T (TLRef (plus (plus n k) h)) (lift k e t0))) (eq_ind_r T (TLRef
+(plus (plus n h) k)) (\lambda (t0: T).(eq T (TLRef (plus (plus n k) h)) t0))
+(f_equal nat T TLRef (plus (plus n k) h) (plus (plus n h) k)
+(plus_permute_2_in_3 n k h)) (lift k e (TLRef (plus n h))) (lift_lref_ge
+(plus n h) k e (le_plus_trans e n h H0))) (lift h d (TLRef n)) (lift_lref_ge
+n h d H1)) (lift h (plus d k) (TLRef (plus n k))) (lift_lref_ge (plus n k) h
+(plus d k) (le_plus_plus d n k k H1 (le_n k)))))) (plus k d) (plus_sym k d))
+(lift k e (TLRef n)) (lift_lref_ge n k e H0)))))))))) (\lambda (k: