1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "basic_1/lift/props.ma".
19 include "basic_1/tlt/props.ma".
21 theorem lift_weight_map:
22 \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to
23 nat))).(((\forall (m: nat).((le d m) \to (eq nat (f m) O)))) \to (eq nat
24 (weight_map f (lift h d t)) (weight_map f t))))))
26 \lambda (t: T).(let TMP_4 \def (\lambda (t0: T).(\forall (h: nat).(\forall
27 (d: nat).(\forall (f: ((nat \to nat))).(((\forall (m: nat).((le d m) \to (eq
28 nat (f m) O)))) \to (let TMP_1 \def (lift h d t0) in (let TMP_2 \def
29 (weight_map f TMP_1) in (let TMP_3 \def (weight_map f t0) in (eq nat TMP_2
30 TMP_3))))))))) in (let TMP_7 \def (\lambda (n: nat).(\lambda (_:
31 nat).(\lambda (d: nat).(\lambda (f: ((nat \to nat))).(\lambda (_: ((\forall
32 (m: nat).((le d m) \to (eq nat (f m) O))))).(let TMP_5 \def (TSort n) in (let
33 TMP_6 \def (weight_map f TMP_5) in (refl_equal nat TMP_6)))))))) in (let
34 TMP_45 \def (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda
35 (f: ((nat \to nat))).(\lambda (H: ((\forall (m: nat).((le d m) \to (eq nat (f
36 m) O))))).(let TMP_8 \def (TLRef n) in (let TMP_9 \def (lift h d TMP_8) in
37 (let TMP_10 \def (weight_map f TMP_9) in (let TMP_11 \def (TLRef n) in (let
38 TMP_12 \def (weight_map f TMP_11) in (let TMP_13 \def (eq nat TMP_10 TMP_12)
39 in (let TMP_25 \def (\lambda (H0: (lt n d)).(let TMP_14 \def (TLRef n) in
40 (let TMP_18 \def (\lambda (t0: T).(let TMP_15 \def (weight_map f t0) in (let
41 TMP_16 \def (TLRef n) in (let TMP_17 \def (weight_map f TMP_16) in (eq nat
42 TMP_15 TMP_17))))) in (let TMP_19 \def (TLRef n) in (let TMP_20 \def
43 (weight_map f TMP_19) in (let TMP_21 \def (refl_equal nat TMP_20) in (let
44 TMP_22 \def (TLRef n) in (let TMP_23 \def (lift h d TMP_22) in (let TMP_24
45 \def (lift_lref_lt n h d H0) in (eq_ind_r T TMP_14 TMP_18 TMP_21 TMP_23
46 TMP_24)))))))))) in (let TMP_44 \def (\lambda (H0: (le d n)).(let TMP_26 \def
47 (plus n h) in (let TMP_27 \def (TLRef TMP_26) in (let TMP_31 \def (\lambda
48 (t0: T).(let TMP_28 \def (weight_map f t0) in (let TMP_29 \def (TLRef n) in
49 (let TMP_30 \def (weight_map f TMP_29) in (eq nat TMP_28 TMP_30))))) in (let
50 TMP_34 \def (\lambda (n0: nat).(let TMP_32 \def (plus n h) in (let TMP_33
51 \def (f TMP_32) in (eq nat TMP_33 n0)))) in (let TMP_35 \def (plus n h) in
52 (let TMP_36 \def (le_plus_trans d n h H0) in (let TMP_37 \def (H TMP_35
53 TMP_36) in (let TMP_38 \def (f n) in (let TMP_39 \def (H n H0) in (let TMP_40
54 \def (eq_ind_r nat O TMP_34 TMP_37 TMP_38 TMP_39) in (let TMP_41 \def (TLRef
55 n) in (let TMP_42 \def (lift h d TMP_41) in (let TMP_43 \def (lift_lref_ge n
56 h d H0) in (eq_ind_r T TMP_27 TMP_31 TMP_40 TMP_42 TMP_43))))))))))))))) in
57 (lt_le_e n d TMP_13 TMP_25 TMP_44)))))))))))))) in (let TMP_325 \def (\lambda
58 (k: K).(\lambda (t0: T).(\lambda (H: ((\forall (h: nat).(\forall (d:
59 nat).(\forall (f: ((nat \to nat))).(((\forall (m: nat).((le d m) \to (eq nat
60 (f m) O)))) \to (eq nat (weight_map f (lift h d t0)) (weight_map f
61 t0)))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (h: nat).(\forall (d:
62 nat).(\forall (f: ((nat \to nat))).(((\forall (m: nat).((le d m) \to (eq nat
63 (f m) O)))) \to (eq nat (weight_map f (lift h d t1)) (weight_map f
64 t1)))))))).(\lambda (h: nat).(\lambda (d: nat).(\lambda (f: ((nat \to
65 nat))).(\lambda (H1: ((\forall (m: nat).((le d m) \to (eq nat (f m)
66 O))))).(let TMP_51 \def (\lambda (k0: K).(let TMP_46 \def (THead k0 t0 t1) in
67 (let TMP_47 \def (lift h d TMP_46) in (let TMP_48 \def (weight_map f TMP_47)
68 in (let TMP_49 \def (THead k0 t0 t1) in (let TMP_50 \def (weight_map f
69 TMP_49) in (eq nat TMP_48 TMP_50))))))) in (let TMP_289 \def (\lambda (b:
70 B).(let TMP_52 \def (Bind b) in (let TMP_53 \def (lift h d t0) in (let TMP_54
71 \def (Bind b) in (let TMP_55 \def (s TMP_54 d) in (let TMP_56 \def (lift h
72 TMP_55 t1) in (let TMP_57 \def (THead TMP_52 TMP_53 TMP_56) in (let TMP_62
73 \def (\lambda (t2: T).(let TMP_58 \def (weight_map f t2) in (let TMP_59 \def
74 (Bind b) in (let TMP_60 \def (THead TMP_59 t0 t1) in (let TMP_61 \def
75 (weight_map f TMP_60) in (eq nat TMP_58 TMP_61)))))) in (let TMP_103 \def
76 (\lambda (b0: B).(let TMP_87 \def (match b0 with [Abbr \Rightarrow (let
77 TMP_77 \def (lift h d t0) in (let TMP_78 \def (weight_map f TMP_77) in (let
78 TMP_79 \def (lift h d t0) in (let TMP_80 \def (weight_map f TMP_79) in (let
79 TMP_81 \def (S TMP_80) in (let TMP_82 \def (wadd f TMP_81) in (let TMP_83
80 \def (S d) in (let TMP_84 \def (lift h TMP_83 t1) in (let TMP_85 \def
81 (weight_map TMP_82 TMP_84) in (let TMP_86 \def (plus TMP_78 TMP_85) in (S
82 TMP_86))))))))))) | Abst \Rightarrow (let TMP_70 \def (lift h d t0) in (let
83 TMP_71 \def (weight_map f TMP_70) in (let TMP_72 \def (wadd f O) in (let
84 TMP_73 \def (S d) in (let TMP_74 \def (lift h TMP_73 t1) in (let TMP_75 \def
85 (weight_map TMP_72 TMP_74) in (let TMP_76 \def (plus TMP_71 TMP_75) in (S
86 TMP_76)))))))) | Void \Rightarrow (let TMP_63 \def (lift h d t0) in (let
87 TMP_64 \def (weight_map f TMP_63) in (let TMP_65 \def (wadd f O) in (let
88 TMP_66 \def (S d) in (let TMP_67 \def (lift h TMP_66 t1) in (let TMP_68 \def
89 (weight_map TMP_65 TMP_67) in (let TMP_69 \def (plus TMP_64 TMP_68) in (S
90 TMP_69))))))))]) in (let TMP_102 \def (match b0 with [Abbr \Rightarrow (let
91 TMP_96 \def (weight_map f t0) in (let TMP_97 \def (weight_map f t0) in (let
92 TMP_98 \def (S TMP_97) in (let TMP_99 \def (wadd f TMP_98) in (let TMP_100
93 \def (weight_map TMP_99 t1) in (let TMP_101 \def (plus TMP_96 TMP_100) in (S
94 TMP_101))))))) | Abst \Rightarrow (let TMP_92 \def (weight_map f t0) in (let
95 TMP_93 \def (wadd f O) in (let TMP_94 \def (weight_map TMP_93 t1) in (let
96 TMP_95 \def (plus TMP_92 TMP_94) in (S TMP_95))))) | Void \Rightarrow (let
97 TMP_88 \def (weight_map f t0) in (let TMP_89 \def (wadd f O) in (let TMP_90
98 \def (weight_map TMP_89 t1) in (let TMP_91 \def (plus TMP_88 TMP_90) in (S
99 TMP_91)))))]) in (eq nat TMP_87 TMP_102)))) in (let TMP_104 \def (weight_map
100 f t0) in (let TMP_119 \def (\lambda (n: nat).(let TMP_105 \def (S n) in (let
101 TMP_106 \def (wadd f TMP_105) in (let TMP_107 \def (S d) in (let TMP_108 \def
102 (lift h TMP_107 t1) in (let TMP_109 \def (weight_map TMP_106 TMP_108) in (let
103 TMP_110 \def (plus n TMP_109) in (let TMP_111 \def (S TMP_110) in (let
104 TMP_112 \def (weight_map f t0) in (let TMP_113 \def (weight_map f t0) in (let
105 TMP_114 \def (S TMP_113) in (let TMP_115 \def (wadd f TMP_114) in (let
106 TMP_116 \def (weight_map TMP_115 t1) in (let TMP_117 \def (plus TMP_112
107 TMP_116) in (let TMP_118 \def (S TMP_117) in (eq nat TMP_111
108 TMP_118)))))))))))))))) in (let TMP_120 \def (weight_map f t0) in (let
109 TMP_121 \def (S TMP_120) in (let TMP_122 \def (wadd f TMP_121) in (let
110 TMP_123 \def (weight_map TMP_122 t1) in (let TMP_134 \def (\lambda (n:
111 nat).(let TMP_124 \def (weight_map f t0) in (let TMP_125 \def (plus TMP_124
112 n) in (let TMP_126 \def (S TMP_125) in (let TMP_127 \def (weight_map f t0) in
113 (let TMP_128 \def (weight_map f t0) in (let TMP_129 \def (S TMP_128) in (let
114 TMP_130 \def (wadd f TMP_129) in (let TMP_131 \def (weight_map TMP_130 t1) in
115 (let TMP_132 \def (plus TMP_127 TMP_131) in (let TMP_133 \def (S TMP_132) in
116 (eq nat TMP_126 TMP_133)))))))))))) in (let TMP_135 \def (weight_map f t0) in
117 (let TMP_136 \def (weight_map f t0) in (let TMP_137 \def (S TMP_136) in (let
118 TMP_138 \def (wadd f TMP_137) in (let TMP_139 \def (weight_map TMP_138 t1) in
119 (let TMP_140 \def (plus TMP_135 TMP_139) in (let TMP_141 \def (S TMP_140) in
120 (let TMP_142 \def (refl_equal nat TMP_141) in (let TMP_143 \def (weight_map f
121 t0) in (let TMP_144 \def (S TMP_143) in (let TMP_145 \def (wadd f TMP_144) in
122 (let TMP_146 \def (S d) in (let TMP_147 \def (lift h TMP_146 t1) in (let
123 TMP_148 \def (weight_map TMP_145 TMP_147) in (let TMP_149 \def (S d) in (let
124 TMP_150 \def (weight_map f t0) in (let TMP_151 \def (S TMP_150) in (let
125 TMP_152 \def (wadd f TMP_151) in (let TMP_168 \def (\lambda (m: nat).(\lambda
126 (H2: (le (S d) m)).(let TMP_154 \def (\lambda (n: nat).(let TMP_153 \def (S
127 n) in (eq nat m TMP_153))) in (let TMP_155 \def (\lambda (n: nat).(le d n))
128 in (let TMP_156 \def (weight_map f t0) in (let TMP_157 \def (S TMP_156) in
129 (let TMP_158 \def (wadd f TMP_157 m) in (let TMP_159 \def (eq nat TMP_158 O)
130 in (let TMP_166 \def (\lambda (x: nat).(\lambda (H3: (eq nat m (S
131 x))).(\lambda (H4: (le d x)).(let TMP_160 \def (S x) in (let TMP_164 \def
132 (\lambda (n: nat).(let TMP_161 \def (weight_map f t0) in (let TMP_162 \def (S
133 TMP_161) in (let TMP_163 \def (wadd f TMP_162 n) in (eq nat TMP_163 O))))) in
134 (let TMP_165 \def (H1 x H4) in (eq_ind_r nat TMP_160 TMP_164 TMP_165 m
135 H3))))))) in (let TMP_167 \def (le_gen_S d m H2) in (ex2_ind nat TMP_154
136 TMP_155 TMP_159 TMP_166 TMP_167))))))))))) in (let TMP_169 \def (H0 h TMP_149
137 TMP_152 TMP_168) in (let TMP_170 \def (eq_ind_r nat TMP_123 TMP_134 TMP_142
138 TMP_148 TMP_169) in (let TMP_171 \def (lift h d t0) in (let TMP_172 \def
139 (weight_map f TMP_171) in (let TMP_173 \def (H h d f H1) in (let TMP_174 \def
140 (eq_ind_r nat TMP_104 TMP_119 TMP_170 TMP_172 TMP_173) in (let TMP_175 \def
141 (wadd f O) in (let TMP_176 \def (weight_map TMP_175 t1) in (let TMP_186 \def
142 (\lambda (n: nat).(let TMP_177 \def (lift h d t0) in (let TMP_178 \def
143 (weight_map f TMP_177) in (let TMP_179 \def (plus TMP_178 n) in (let TMP_180
144 \def (S TMP_179) in (let TMP_181 \def (weight_map f t0) in (let TMP_182 \def
145 (wadd f O) in (let TMP_183 \def (weight_map TMP_182 t1) in (let TMP_184 \def
146 (plus TMP_181 TMP_183) in (let TMP_185 \def (S TMP_184) in (eq nat TMP_180
147 TMP_185))))))))))) in (let TMP_187 \def (lift h d t0) in (let TMP_188 \def
148 (weight_map f TMP_187) in (let TMP_189 \def (wadd f O) in (let TMP_190 \def
149 (weight_map TMP_189 t1) in (let TMP_191 \def (plus TMP_188 TMP_190) in (let
150 TMP_192 \def (weight_map f t0) in (let TMP_193 \def (wadd f O) in (let
151 TMP_194 \def (weight_map TMP_193 t1) in (let TMP_195 \def (plus TMP_192
152 TMP_194) in (let TMP_196 \def (lift h d t0) in (let TMP_197 \def (weight_map
153 f TMP_196) in (let TMP_198 \def (weight_map f t0) in (let TMP_199 \def (wadd
154 f O) in (let TMP_200 \def (weight_map TMP_199 t1) in (let TMP_201 \def (wadd
155 f O) in (let TMP_202 \def (weight_map TMP_201 t1) in (let TMP_203 \def (H h d
156 f H1) in (let TMP_204 \def (wadd f O) in (let TMP_205 \def (weight_map
157 TMP_204 t1) in (let TMP_206 \def (refl_equal nat TMP_205) in (let TMP_207
158 \def (f_equal2 nat nat nat plus TMP_197 TMP_198 TMP_200 TMP_202 TMP_203
159 TMP_206) in (let TMP_208 \def (f_equal nat nat S TMP_191 TMP_195 TMP_207) in
160 (let TMP_209 \def (wadd f O) in (let TMP_210 \def (S d) in (let TMP_211 \def
161 (lift h TMP_210 t1) in (let TMP_212 \def (weight_map TMP_209 TMP_211) in (let
162 TMP_213 \def (S d) in (let TMP_214 \def (wadd f O) in (let TMP_226 \def
163 (\lambda (m: nat).(\lambda (H2: (le (S d) m)).(let TMP_216 \def (\lambda (n:
164 nat).(let TMP_215 \def (S n) in (eq nat m TMP_215))) in (let TMP_217 \def
165 (\lambda (n: nat).(le d n)) in (let TMP_218 \def (wadd f O m) in (let TMP_219
166 \def (eq nat TMP_218 O) in (let TMP_224 \def (\lambda (x: nat).(\lambda (H3:
167 (eq nat m (S x))).(\lambda (H4: (le d x)).(let TMP_220 \def (S x) in (let
168 TMP_222 \def (\lambda (n: nat).(let TMP_221 \def (wadd f O n) in (eq nat
169 TMP_221 O))) in (let TMP_223 \def (H1 x H4) in (eq_ind_r nat TMP_220 TMP_222
170 TMP_223 m H3))))))) in (let TMP_225 \def (le_gen_S d m H2) in (ex2_ind nat
171 TMP_216 TMP_217 TMP_219 TMP_224 TMP_225))))))))) in (let TMP_227 \def (H0 h
172 TMP_213 TMP_214 TMP_226) in (let TMP_228 \def (eq_ind_r nat TMP_176 TMP_186
173 TMP_208 TMP_212 TMP_227) in (let TMP_229 \def (wadd f O) in (let TMP_230 \def
174 (weight_map TMP_229 t1) in (let TMP_240 \def (\lambda (n: nat).(let TMP_231
175 \def (lift h d t0) in (let TMP_232 \def (weight_map f TMP_231) in (let
176 TMP_233 \def (plus TMP_232 n) in (let TMP_234 \def (S TMP_233) in (let
177 TMP_235 \def (weight_map f t0) in (let TMP_236 \def (wadd f O) in (let
178 TMP_237 \def (weight_map TMP_236 t1) in (let TMP_238 \def (plus TMP_235
179 TMP_237) in (let TMP_239 \def (S TMP_238) in (eq nat TMP_234
180 TMP_239))))))))))) in (let TMP_241 \def (lift h d t0) in (let TMP_242 \def
181 (weight_map f TMP_241) in (let TMP_243 \def (wadd f O) in (let TMP_244 \def
182 (weight_map TMP_243 t1) in (let TMP_245 \def (plus TMP_242 TMP_244) in (let
183 TMP_246 \def (weight_map f t0) in (let TMP_247 \def (wadd f O) in (let
184 TMP_248 \def (weight_map TMP_247 t1) in (let TMP_249 \def (plus TMP_246
185 TMP_248) in (let TMP_250 \def (lift h d t0) in (let TMP_251 \def (weight_map
186 f TMP_250) in (let TMP_252 \def (weight_map f t0) in (let TMP_253 \def (wadd
187 f O) in (let TMP_254 \def (weight_map TMP_253 t1) in (let TMP_255 \def (wadd
188 f O) in (let TMP_256 \def (weight_map TMP_255 t1) in (let TMP_257 \def (H h d
189 f H1) in (let TMP_258 \def (wadd f O) in (let TMP_259 \def (weight_map
190 TMP_258 t1) in (let TMP_260 \def (refl_equal nat TMP_259) in (let TMP_261
191 \def (f_equal2 nat nat nat plus TMP_251 TMP_252 TMP_254 TMP_256 TMP_257
192 TMP_260) in (let TMP_262 \def (f_equal nat nat S TMP_245 TMP_249 TMP_261) in
193 (let TMP_263 \def (wadd f O) in (let TMP_264 \def (S d) in (let TMP_265 \def
194 (lift h TMP_264 t1) in (let TMP_266 \def (weight_map TMP_263 TMP_265) in (let
195 TMP_267 \def (S d) in (let TMP_268 \def (wadd f O) in (let TMP_280 \def
196 (\lambda (m: nat).(\lambda (H2: (le (S d) m)).(let TMP_270 \def (\lambda (n:
197 nat).(let TMP_269 \def (S n) in (eq nat m TMP_269))) in (let TMP_271 \def
198 (\lambda (n: nat).(le d n)) in (let TMP_272 \def (wadd f O m) in (let TMP_273
199 \def (eq nat TMP_272 O) in (let TMP_278 \def (\lambda (x: nat).(\lambda (H3:
200 (eq nat m (S x))).(\lambda (H4: (le d x)).(let TMP_274 \def (S x) in (let
201 TMP_276 \def (\lambda (n: nat).(let TMP_275 \def (wadd f O n) in (eq nat
202 TMP_275 O))) in (let TMP_277 \def (H1 x H4) in (eq_ind_r nat TMP_274 TMP_276
203 TMP_277 m H3))))))) in (let TMP_279 \def (le_gen_S d m H2) in (ex2_ind nat
204 TMP_270 TMP_271 TMP_273 TMP_278 TMP_279))))))))) in (let TMP_281 \def (H0 h
205 TMP_267 TMP_268 TMP_280) in (let TMP_282 \def (eq_ind_r nat TMP_230 TMP_240
206 TMP_262 TMP_266 TMP_281) in (let TMP_283 \def (B_ind TMP_103 TMP_174 TMP_228
207 TMP_282 b) in (let TMP_284 \def (Bind b) in (let TMP_285 \def (THead TMP_284
208 t0 t1) in (let TMP_286 \def (lift h d TMP_285) in (let TMP_287 \def (Bind b)
209 in (let TMP_288 \def (lift_head TMP_287 t0 t1 h d) in (eq_ind_r T TMP_57
210 TMP_62 TMP_283 TMP_286
211 TMP_288)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
212 ))))))))))))))))))))))))))))))))))))))))))))) in (let TMP_324 \def (\lambda
213 (f0: F).(let TMP_290 \def (Flat f0) in (let TMP_291 \def (lift h d t0) in
214 (let TMP_292 \def (Flat f0) in (let TMP_293 \def (s TMP_292 d) in (let
215 TMP_294 \def (lift h TMP_293 t1) in (let TMP_295 \def (THead TMP_290 TMP_291
216 TMP_294) in (let TMP_300 \def (\lambda (t2: T).(let TMP_296 \def (weight_map
217 f t2) in (let TMP_297 \def (Flat f0) in (let TMP_298 \def (THead TMP_297 t0
218 t1) in (let TMP_299 \def (weight_map f TMP_298) in (eq nat TMP_296
219 TMP_299)))))) in (let TMP_301 \def (lift h d t0) in (let TMP_302 \def
220 (weight_map f TMP_301) in (let TMP_303 \def (lift h d t1) in (let TMP_304
221 \def (weight_map f TMP_303) in (let TMP_305 \def (plus TMP_302 TMP_304) in
222 (let TMP_306 \def (weight_map f t0) in (let TMP_307 \def (weight_map f t1) in
223 (let TMP_308 \def (plus TMP_306 TMP_307) in (let TMP_309 \def (lift h d t0)
224 in (let TMP_310 \def (weight_map f TMP_309) in (let TMP_311 \def (weight_map
225 f t0) in (let TMP_312 \def (lift h d t1) in (let TMP_313 \def (weight_map f
226 TMP_312) in (let TMP_314 \def (weight_map f t1) in (let TMP_315 \def (H h d f
227 H1) in (let TMP_316 \def (H0 h d f H1) in (let TMP_317 \def (f_equal2 nat nat
228 nat plus TMP_310 TMP_311 TMP_313 TMP_314 TMP_315 TMP_316) in (let TMP_318
229 \def (f_equal nat nat S TMP_305 TMP_308 TMP_317) in (let TMP_319 \def (Flat
230 f0) in (let TMP_320 \def (THead TMP_319 t0 t1) in (let TMP_321 \def (lift h d
231 TMP_320) in (let TMP_322 \def (Flat f0) in (let TMP_323 \def (lift_head
232 TMP_322 t0 t1 h d) in (eq_ind_r T TMP_295 TMP_300 TMP_318 TMP_321
233 TMP_323)))))))))))))))))))))))))))))))) in (K_ind TMP_51 TMP_289 TMP_324
234 k))))))))))))) in (T_ind TMP_4 TMP_7 TMP_45 TMP_325 t))))).
237 \forall (t: T).(\forall (h: nat).(\forall (d: nat).(eq nat (weight (lift h d
240 \lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(let TMP_1 \def (\lambda
241 (_: nat).O) in (let TMP_2 \def (\lambda (m: nat).(\lambda (_: (le d
242 m)).(refl_equal nat O))) in (lift_weight_map t h d TMP_1 TMP_2))))).
244 theorem lift_weight_add:
245 \forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (d:
246 nat).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
247 (m: nat).((lt m d) \to (eq nat (g m) (f m))))) \to ((eq nat (g d) w) \to
248 (((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m))))) \to (eq nat
249 (weight_map f (lift h d t)) (weight_map g (lift (S h) d t)))))))))))
251 \lambda (w: nat).(\lambda (t: T).(let TMP_6 \def (\lambda (t0: T).(\forall
252 (h: nat).(\forall (d: nat).(\forall (f: ((nat \to nat))).(\forall (g: ((nat
253 \to nat))).(((\forall (m: nat).((lt m d) \to (eq nat (g m) (f m))))) \to ((eq
254 nat (g d) w) \to (((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f
255 m))))) \to (let TMP_1 \def (lift h d t0) in (let TMP_2 \def (weight_map f
256 TMP_1) in (let TMP_3 \def (S h) in (let TMP_4 \def (lift TMP_3 d t0) in (let
257 TMP_5 \def (weight_map g TMP_4) in (eq nat TMP_2 TMP_5)))))))))))))) in (let
258 TMP_11 \def (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda
259 (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (_: ((\forall (m:
260 nat).((lt m d) \to (eq nat (g m) (f m)))))).(\lambda (_: (eq nat (g d)
261 w)).(\lambda (_: ((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f
262 m)))))).(let TMP_7 \def (S h) in (let TMP_8 \def (TSort n) in (let TMP_9 \def
263 (lift TMP_7 d TMP_8) in (let TMP_10 \def (weight_map g TMP_9) in (refl_equal
264 nat TMP_10))))))))))))) in (let TMP_91 \def (\lambda (n: nat).(\lambda (h:
265 nat).(\lambda (d: nat).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
266 nat))).(\lambda (H: ((\forall (m: nat).((lt m d) \to (eq nat (g m) (f
267 m)))))).(\lambda (_: (eq nat (g d) w)).(\lambda (H1: ((\forall (m: nat).((le
268 d m) \to (eq nat (g (S m)) (f m)))))).(let TMP_12 \def (TLRef n) in (let
269 TMP_13 \def (lift h d TMP_12) in (let TMP_14 \def (weight_map f TMP_13) in
270 (let TMP_15 \def (S h) in (let TMP_16 \def (TLRef n) in (let TMP_17 \def
271 (lift TMP_15 d TMP_16) in (let TMP_18 \def (weight_map g TMP_17) in (let
272 TMP_19 \def (eq nat TMP_14 TMP_18) in (let TMP_45 \def (\lambda (H2: (lt n
273 d)).(let TMP_20 \def (TLRef n) in (let TMP_26 \def (\lambda (t0: T).(let
274 TMP_21 \def (weight_map f t0) in (let TMP_22 \def (S h) in (let TMP_23 \def
275 (TLRef n) in (let TMP_24 \def (lift TMP_22 d TMP_23) in (let TMP_25 \def
276 (weight_map g TMP_24) in (eq nat TMP_21 TMP_25))))))) in (let TMP_27 \def
277 (TLRef n) in (let TMP_31 \def (\lambda (t0: T).(let TMP_28 \def (TLRef n) in
278 (let TMP_29 \def (weight_map f TMP_28) in (let TMP_30 \def (weight_map g t0)
279 in (eq nat TMP_29 TMP_30))))) in (let TMP_32 \def (g n) in (let TMP_33 \def
280 (f n) in (let TMP_34 \def (H n H2) in (let TMP_35 \def (sym_eq nat TMP_32
281 TMP_33 TMP_34) in (let TMP_36 \def (S h) in (let TMP_37 \def (TLRef n) in
282 (let TMP_38 \def (lift TMP_36 d TMP_37) in (let TMP_39 \def (S h) in (let
283 TMP_40 \def (lift_lref_lt n TMP_39 d H2) in (let TMP_41 \def (eq_ind_r T
284 TMP_27 TMP_31 TMP_35 TMP_38 TMP_40) in (let TMP_42 \def (TLRef n) in (let
285 TMP_43 \def (lift h d TMP_42) in (let TMP_44 \def (lift_lref_lt n h d H2) in
286 (eq_ind_r T TMP_20 TMP_26 TMP_41 TMP_43 TMP_44))))))))))))))))))) in (let
287 TMP_90 \def (\lambda (H2: (le d n)).(let TMP_46 \def (plus n h) in (let
288 TMP_47 \def (TLRef TMP_46) in (let TMP_53 \def (\lambda (t0: T).(let TMP_48
289 \def (weight_map f t0) in (let TMP_49 \def (S h) in (let TMP_50 \def (TLRef
290 n) in (let TMP_51 \def (lift TMP_49 d TMP_50) in (let TMP_52 \def (weight_map
291 g TMP_51) in (eq nat TMP_48 TMP_52))))))) in (let TMP_54 \def (S h) in (let
292 TMP_55 \def (plus n TMP_54) in (let TMP_56 \def (TLRef TMP_55) in (let TMP_61
293 \def (\lambda (t0: T).(let TMP_57 \def (plus n h) in (let TMP_58 \def (TLRef
294 TMP_57) in (let TMP_59 \def (weight_map f TMP_58) in (let TMP_60 \def
295 (weight_map g t0) in (eq nat TMP_59 TMP_60)))))) in (let TMP_62 \def (plus n
296 h) in (let TMP_63 \def (S TMP_62) in (let TMP_67 \def (\lambda (n0: nat).(let
297 TMP_64 \def (plus n h) in (let TMP_65 \def (f TMP_64) in (let TMP_66 \def (g
298 n0) in (eq nat TMP_65 TMP_66))))) in (let TMP_68 \def (plus n h) in (let
299 TMP_69 \def (S TMP_68) in (let TMP_70 \def (g TMP_69) in (let TMP_71 \def
300 (plus n h) in (let TMP_72 \def (f TMP_71) in (let TMP_73 \def (plus n h) in
301 (let TMP_74 \def (le_plus_trans d n h H2) in (let TMP_75 \def (H1 TMP_73
302 TMP_74) in (let TMP_76 \def (sym_eq nat TMP_70 TMP_72 TMP_75) in (let TMP_77
303 \def (S h) in (let TMP_78 \def (plus n TMP_77) in (let TMP_79 \def (plus_n_Sm
304 n h) in (let TMP_80 \def (eq_ind nat TMP_63 TMP_67 TMP_76 TMP_78 TMP_79) in
305 (let TMP_81 \def (S h) in (let TMP_82 \def (TLRef n) in (let TMP_83 \def
306 (lift TMP_81 d TMP_82) in (let TMP_84 \def (S h) in (let TMP_85 \def
307 (lift_lref_ge n TMP_84 d H2) in (let TMP_86 \def (eq_ind_r T TMP_56 TMP_61
308 TMP_80 TMP_83 TMP_85) in (let TMP_87 \def (TLRef n) in (let TMP_88 \def (lift
309 h d TMP_87) in (let TMP_89 \def (lift_lref_ge n h d H2) in (eq_ind_r T TMP_47
310 TMP_53 TMP_86 TMP_88 TMP_89)))))))))))))))))))))))))))))))))) in (lt_le_e n d
311 TMP_19 TMP_45 TMP_90))))))))))))))))))) in (let TMP_577 \def (\lambda (k:
312 K).(\lambda (t0: T).(\lambda (H: ((\forall (h: nat).(\forall (d:
313 nat).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
314 (m: nat).((lt m d) \to (eq nat (g m) (f m))))) \to ((eq nat (g d) w) \to
315 (((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m))))) \to (eq nat
316 (weight_map f (lift h d t0)) (weight_map g (lift (S h) d
317 t0)))))))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (h: nat).(\forall (d:
318 nat).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
319 (m: nat).((lt m d) \to (eq nat (g m) (f m))))) \to ((eq nat (g d) w) \to
320 (((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m))))) \to (eq nat
321 (weight_map f (lift h d t1)) (weight_map g (lift (S h) d
322 t1)))))))))))).(\lambda (h: nat).(\lambda (d: nat).(\lambda (f: ((nat \to
323 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (m: nat).((lt m
324 d) \to (eq nat (g m) (f m)))))).(\lambda (H2: (eq nat (g d) w)).(\lambda (H3:
325 ((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m)))))).(let TMP_99
326 \def (\lambda (k0: K).(let TMP_92 \def (THead k0 t0 t1) in (let TMP_93 \def
327 (lift h d TMP_92) in (let TMP_94 \def (weight_map f TMP_93) in (let TMP_95
328 \def (S h) in (let TMP_96 \def (THead k0 t0 t1) in (let TMP_97 \def (lift
329 TMP_95 d TMP_96) in (let TMP_98 \def (weight_map g TMP_97) in (eq nat TMP_94
330 TMP_98))))))))) in (let TMP_506 \def (\lambda (b: B).(let TMP_100 \def (Bind
331 b) in (let TMP_101 \def (lift h d t0) in (let TMP_102 \def (Bind b) in (let
332 TMP_103 \def (s TMP_102 d) in (let TMP_104 \def (lift h TMP_103 t1) in (let
333 TMP_105 \def (THead TMP_100 TMP_101 TMP_104) in (let TMP_112 \def (\lambda
334 (t2: T).(let TMP_106 \def (weight_map f t2) in (let TMP_107 \def (S h) in
335 (let TMP_108 \def (Bind b) in (let TMP_109 \def (THead TMP_108 t0 t1) in (let
336 TMP_110 \def (lift TMP_107 d TMP_109) in (let TMP_111 \def (weight_map g
337 TMP_110) in (eq nat TMP_106 TMP_111)))))))) in (let TMP_113 \def (Bind b) in
338 (let TMP_114 \def (S h) in (let TMP_115 \def (lift TMP_114 d t0) in (let
339 TMP_116 \def (S h) in (let TMP_117 \def (Bind b) in (let TMP_118 \def (s
340 TMP_117 d) in (let TMP_119 \def (lift TMP_116 TMP_118 t1) in (let TMP_120
341 \def (THead TMP_113 TMP_115 TMP_119) in (let TMP_129 \def (\lambda (t2:
342 T).(let TMP_121 \def (Bind b) in (let TMP_122 \def (lift h d t0) in (let
343 TMP_123 \def (Bind b) in (let TMP_124 \def (s TMP_123 d) in (let TMP_125 \def
344 (lift h TMP_124 t1) in (let TMP_126 \def (THead TMP_121 TMP_122 TMP_125) in
345 (let TMP_127 \def (weight_map f TMP_126) in (let TMP_128 \def (weight_map g
346 t2) in (eq nat TMP_127 TMP_128)))))))))) in (let TMP_187 \def (\lambda (b0:
347 B).(let TMP_154 \def (match b0 with [Abbr \Rightarrow (let TMP_144 \def (lift
348 h d t0) in (let TMP_145 \def (weight_map f TMP_144) in (let TMP_146 \def
349 (lift h d t0) in (let TMP_147 \def (weight_map f TMP_146) in (let TMP_148
350 \def (S TMP_147) in (let TMP_149 \def (wadd f TMP_148) in (let TMP_150 \def
351 (S d) in (let TMP_151 \def (lift h TMP_150 t1) in (let TMP_152 \def
352 (weight_map TMP_149 TMP_151) in (let TMP_153 \def (plus TMP_145 TMP_152) in
353 (S TMP_153))))))))))) | Abst \Rightarrow (let TMP_137 \def (lift h d t0) in
354 (let TMP_138 \def (weight_map f TMP_137) in (let TMP_139 \def (wadd f O) in
355 (let TMP_140 \def (S d) in (let TMP_141 \def (lift h TMP_140 t1) in (let
356 TMP_142 \def (weight_map TMP_139 TMP_141) in (let TMP_143 \def (plus TMP_138
357 TMP_142) in (S TMP_143)))))))) | Void \Rightarrow (let TMP_130 \def (lift h d
358 t0) in (let TMP_131 \def (weight_map f TMP_130) in (let TMP_132 \def (wadd f
359 O) in (let TMP_133 \def (S d) in (let TMP_134 \def (lift h TMP_133 t1) in
360 (let TMP_135 \def (weight_map TMP_132 TMP_134) in (let TMP_136 \def (plus
361 TMP_131 TMP_135) in (S TMP_136))))))))]) in (let TMP_186 \def (match b0 with
362 [Abbr \Rightarrow (let TMP_173 \def (S h) in (let TMP_174 \def (lift TMP_173
363 d t0) in (let TMP_175 \def (weight_map g TMP_174) in (let TMP_176 \def (S h)
364 in (let TMP_177 \def (lift TMP_176 d t0) in (let TMP_178 \def (weight_map g
365 TMP_177) in (let TMP_179 \def (S TMP_178) in (let TMP_180 \def (wadd g
366 TMP_179) in (let TMP_181 \def (S h) in (let TMP_182 \def (S d) in (let
367 TMP_183 \def (lift TMP_181 TMP_182 t1) in (let TMP_184 \def (weight_map
368 TMP_180 TMP_183) in (let TMP_185 \def (plus TMP_175 TMP_184) in (S
369 TMP_185)))))))))))))) | Abst \Rightarrow (let TMP_164 \def (S h) in (let
370 TMP_165 \def (lift TMP_164 d t0) in (let TMP_166 \def (weight_map g TMP_165)
371 in (let TMP_167 \def (wadd g O) in (let TMP_168 \def (S h) in (let TMP_169
372 \def (S d) in (let TMP_170 \def (lift TMP_168 TMP_169 t1) in (let TMP_171
373 \def (weight_map TMP_167 TMP_170) in (let TMP_172 \def (plus TMP_166 TMP_171)
374 in (S TMP_172)))))))))) | Void \Rightarrow (let TMP_155 \def (S h) in (let
375 TMP_156 \def (lift TMP_155 d t0) in (let TMP_157 \def (weight_map g TMP_156)
376 in (let TMP_158 \def (wadd g O) in (let TMP_159 \def (S h) in (let TMP_160
377 \def (S d) in (let TMP_161 \def (lift TMP_159 TMP_160 t1) in (let TMP_162
378 \def (weight_map TMP_158 TMP_161) in (let TMP_163 \def (plus TMP_157 TMP_162)
379 in (S TMP_163))))))))))]) in (eq nat TMP_154 TMP_186)))) in (let TMP_188 \def
380 (lift h d t0) in (let TMP_189 \def (weight_map f TMP_188) in (let TMP_190
381 \def (lift h d t0) in (let TMP_191 \def (weight_map f TMP_190) in (let
382 TMP_192 \def (S TMP_191) in (let TMP_193 \def (wadd f TMP_192) in (let
383 TMP_194 \def (S d) in (let TMP_195 \def (lift h TMP_194 t1) in (let TMP_196
384 \def (weight_map TMP_193 TMP_195) in (let TMP_197 \def (plus TMP_189 TMP_196)
385 in (let TMP_198 \def (S h) in (let TMP_199 \def (lift TMP_198 d t0) in (let
386 TMP_200 \def (weight_map g TMP_199) in (let TMP_201 \def (S h) in (let
387 TMP_202 \def (lift TMP_201 d t0) in (let TMP_203 \def (weight_map g TMP_202)
388 in (let TMP_204 \def (S TMP_203) in (let TMP_205 \def (wadd g TMP_204) in
389 (let TMP_206 \def (S h) in (let TMP_207 \def (S d) in (let TMP_208 \def (lift
390 TMP_206 TMP_207 t1) in (let TMP_209 \def (weight_map TMP_205 TMP_208) in (let
391 TMP_210 \def (plus TMP_200 TMP_209) in (let TMP_211 \def (lift h d t0) in
392 (let TMP_212 \def (weight_map f TMP_211) in (let TMP_213 \def (S h) in (let
393 TMP_214 \def (lift TMP_213 d t0) in (let TMP_215 \def (weight_map g TMP_214)
394 in (let TMP_216 \def (lift h d t0) in (let TMP_217 \def (weight_map f
395 TMP_216) in (let TMP_218 \def (S TMP_217) in (let TMP_219 \def (wadd f
396 TMP_218) in (let TMP_220 \def (S d) in (let TMP_221 \def (lift h TMP_220 t1)
397 in (let TMP_222 \def (weight_map TMP_219 TMP_221) in (let TMP_223 \def (S h)
398 in (let TMP_224 \def (lift TMP_223 d t0) in (let TMP_225 \def (weight_map g
399 TMP_224) in (let TMP_226 \def (S TMP_225) in (let TMP_227 \def (wadd g
400 TMP_226) in (let TMP_228 \def (S h) in (let TMP_229 \def (S d) in (let
401 TMP_230 \def (lift TMP_228 TMP_229 t1) in (let TMP_231 \def (weight_map
402 TMP_227 TMP_230) in (let TMP_232 \def (H h d f g H1 H2 H3) in (let TMP_233
403 \def (S d) in (let TMP_234 \def (lift h d t0) in (let TMP_235 \def
404 (weight_map f TMP_234) in (let TMP_236 \def (S TMP_235) in (let TMP_237 \def
405 (wadd f TMP_236) in (let TMP_238 \def (S h) in (let TMP_239 \def (lift
406 TMP_238 d t0) in (let TMP_240 \def (weight_map g TMP_239) in (let TMP_241
407 \def (S TMP_240) in (let TMP_242 \def (wadd g TMP_241) in (let TMP_310 \def
408 (\lambda (m: nat).(\lambda (H4: (lt m (S d))).(let TMP_243 \def (eq nat m O)
409 in (let TMP_245 \def (\lambda (m0: nat).(let TMP_244 \def (S m0) in (eq nat m
410 TMP_244))) in (let TMP_246 \def (\lambda (m0: nat).(lt m0 d)) in (let TMP_247
411 \def (ex2 nat TMP_245 TMP_246) in (let TMP_248 \def (S h) in (let TMP_249
412 \def (lift TMP_248 d t0) in (let TMP_250 \def (weight_map g TMP_249) in (let
413 TMP_251 \def (S TMP_250) in (let TMP_252 \def (wadd g TMP_251 m) in (let
414 TMP_253 \def (lift h d t0) in (let TMP_254 \def (weight_map f TMP_253) in
415 (let TMP_255 \def (S TMP_254) in (let TMP_256 \def (wadd f TMP_255 m) in (let
416 TMP_257 \def (eq nat TMP_252 TMP_256) in (let TMP_281 \def (\lambda (H5: (eq
417 nat m O)).(let TMP_267 \def (\lambda (n: nat).(let TMP_258 \def (S h) in (let
418 TMP_259 \def (lift TMP_258 d t0) in (let TMP_260 \def (weight_map g TMP_259)
419 in (let TMP_261 \def (S TMP_260) in (let TMP_262 \def (wadd g TMP_261 n) in
420 (let TMP_263 \def (lift h d t0) in (let TMP_264 \def (weight_map f TMP_263)
421 in (let TMP_265 \def (S TMP_264) in (let TMP_266 \def (wadd f TMP_265 n) in
422 (eq nat TMP_262 TMP_266))))))))))) in (let TMP_268 \def (S h) in (let TMP_269
423 \def (lift TMP_268 d t0) in (let TMP_270 \def (weight_map g TMP_269) in (let
424 TMP_271 \def (lift h d t0) in (let TMP_272 \def (weight_map f TMP_271) in
425 (let TMP_273 \def (lift h d t0) in (let TMP_274 \def (weight_map f TMP_273)
426 in (let TMP_275 \def (S h) in (let TMP_276 \def (lift TMP_275 d t0) in (let
427 TMP_277 \def (weight_map g TMP_276) in (let TMP_278 \def (H h d f g H1 H2 H3)
428 in (let TMP_279 \def (sym_eq nat TMP_274 TMP_277 TMP_278) in (let TMP_280
429 \def (f_equal nat nat S TMP_270 TMP_272 TMP_279) in (eq_ind_r nat O TMP_267
430 TMP_280 m H5)))))))))))))))) in (let TMP_308 \def (\lambda (H5: (ex2 nat
431 (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d)))).(let
432 TMP_283 \def (\lambda (m0: nat).(let TMP_282 \def (S m0) in (eq nat m
433 TMP_282))) in (let TMP_284 \def (\lambda (m0: nat).(lt m0 d)) in (let TMP_285
434 \def (S h) in (let TMP_286 \def (lift TMP_285 d t0) in (let TMP_287 \def
435 (weight_map g TMP_286) in (let TMP_288 \def (S TMP_287) in (let TMP_289 \def
436 (wadd g TMP_288 m) in (let TMP_290 \def (lift h d t0) in (let TMP_291 \def
437 (weight_map f TMP_290) in (let TMP_292 \def (S TMP_291) in (let TMP_293 \def
438 (wadd f TMP_292 m) in (let TMP_294 \def (eq nat TMP_289 TMP_293) in (let
439 TMP_307 \def (\lambda (x: nat).(\lambda (H6: (eq nat m (S x))).(\lambda (H7:
440 (lt x d)).(let TMP_295 \def (S x) in (let TMP_305 \def (\lambda (n: nat).(let
441 TMP_296 \def (S h) in (let TMP_297 \def (lift TMP_296 d t0) in (let TMP_298
442 \def (weight_map g TMP_297) in (let TMP_299 \def (S TMP_298) in (let TMP_300
443 \def (wadd g TMP_299 n) in (let TMP_301 \def (lift h d t0) in (let TMP_302
444 \def (weight_map f TMP_301) in (let TMP_303 \def (S TMP_302) in (let TMP_304
445 \def (wadd f TMP_303 n) in (eq nat TMP_300 TMP_304))))))))))) in (let TMP_306
446 \def (H1 x H7) in (eq_ind_r nat TMP_295 TMP_305 TMP_306 m H6))))))) in
447 (ex2_ind nat TMP_283 TMP_284 TMP_294 TMP_307 H5))))))))))))))) in (let
448 TMP_309 \def (lt_gen_xS m d H4) in (or_ind TMP_243 TMP_247 TMP_257 TMP_281
449 TMP_308 TMP_309)))))))))))))))))))) in (let TMP_330 \def (\lambda (m:
450 nat).(\lambda (H4: (le (S d) m)).(let TMP_312 \def (\lambda (n: nat).(let
451 TMP_311 \def (S n) in (eq nat m TMP_311))) in (let TMP_313 \def (\lambda (n:
452 nat).(le d n)) in (let TMP_314 \def (g m) in (let TMP_315 \def (lift h d t0)
453 in (let TMP_316 \def (weight_map f TMP_315) in (let TMP_317 \def (S TMP_316)
454 in (let TMP_318 \def (wadd f TMP_317 m) in (let TMP_319 \def (eq nat TMP_314
455 TMP_318) in (let TMP_328 \def (\lambda (x: nat).(\lambda (H5: (eq nat m (S
456 x))).(\lambda (H6: (le d x)).(let TMP_320 \def (S x) in (let TMP_326 \def
457 (\lambda (n: nat).(let TMP_321 \def (g n) in (let TMP_322 \def (lift h d t0)
458 in (let TMP_323 \def (weight_map f TMP_322) in (let TMP_324 \def (S TMP_323)
459 in (let TMP_325 \def (wadd f TMP_324 n) in (eq nat TMP_321 TMP_325))))))) in
460 (let TMP_327 \def (H3 x H6) in (eq_ind_r nat TMP_320 TMP_326 TMP_327 m
461 H5))))))) in (let TMP_329 \def (le_gen_S d m H4) in (ex2_ind nat TMP_312
462 TMP_313 TMP_319 TMP_328 TMP_329))))))))))))) in (let TMP_331 \def (H0 h
463 TMP_233 TMP_237 TMP_242 TMP_310 H2 TMP_330) in (let TMP_332 \def (f_equal2
464 nat nat nat plus TMP_212 TMP_215 TMP_222 TMP_231 TMP_232 TMP_331) in (let
465 TMP_333 \def (f_equal nat nat S TMP_197 TMP_210 TMP_332) in (let TMP_334 \def
466 (lift h d t0) in (let TMP_335 \def (weight_map f TMP_334) in (let TMP_336
467 \def (wadd f O) in (let TMP_337 \def (S d) in (let TMP_338 \def (lift h
468 TMP_337 t1) in (let TMP_339 \def (weight_map TMP_336 TMP_338) in (let TMP_340
469 \def (plus TMP_335 TMP_339) in (let TMP_341 \def (S h) in (let TMP_342 \def
470 (lift TMP_341 d t0) in (let TMP_343 \def (weight_map g TMP_342) in (let
471 TMP_344 \def (wadd g O) in (let TMP_345 \def (S h) in (let TMP_346 \def (S d)
472 in (let TMP_347 \def (lift TMP_345 TMP_346 t1) in (let TMP_348 \def
473 (weight_map TMP_344 TMP_347) in (let TMP_349 \def (plus TMP_343 TMP_348) in
474 (let TMP_350 \def (lift h d t0) in (let TMP_351 \def (weight_map f TMP_350)
475 in (let TMP_352 \def (S h) in (let TMP_353 \def (lift TMP_352 d t0) in (let
476 TMP_354 \def (weight_map g TMP_353) in (let TMP_355 \def (wadd f O) in (let
477 TMP_356 \def (S d) in (let TMP_357 \def (lift h TMP_356 t1) in (let TMP_358
478 \def (weight_map TMP_355 TMP_357) in (let TMP_359 \def (wadd g O) in (let
479 TMP_360 \def (S h) in (let TMP_361 \def (S d) in (let TMP_362 \def (lift
480 TMP_360 TMP_361 t1) in (let TMP_363 \def (weight_map TMP_359 TMP_362) in (let
481 TMP_364 \def (H h d f g H1 H2 H3) in (let TMP_365 \def (S d) in (let TMP_366
482 \def (wadd f O) in (let TMP_367 \def (wadd g O) in (let TMP_395 \def (\lambda
483 (m: nat).(\lambda (H4: (lt m (S d))).(let TMP_368 \def (eq nat m O) in (let
484 TMP_370 \def (\lambda (m0: nat).(let TMP_369 \def (S m0) in (eq nat m
485 TMP_369))) in (let TMP_371 \def (\lambda (m0: nat).(lt m0 d)) in (let TMP_372
486 \def (ex2 nat TMP_370 TMP_371) in (let TMP_373 \def (wadd g O m) in (let
487 TMP_374 \def (wadd f O m) in (let TMP_375 \def (eq nat TMP_373 TMP_374) in
488 (let TMP_380 \def (\lambda (H5: (eq nat m O)).(let TMP_378 \def (\lambda (n:
489 nat).(let TMP_376 \def (wadd g O n) in (let TMP_377 \def (wadd f O n) in (eq
490 nat TMP_376 TMP_377)))) in (let TMP_379 \def (refl_equal nat O) in (eq_ind_r
491 nat O TMP_378 TMP_379 m H5)))) in (let TMP_393 \def (\lambda (H5: (ex2 nat
492 (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d)))).(let
493 TMP_382 \def (\lambda (m0: nat).(let TMP_381 \def (S m0) in (eq nat m
494 TMP_381))) in (let TMP_383 \def (\lambda (m0: nat).(lt m0 d)) in (let TMP_384
495 \def (wadd g O m) in (let TMP_385 \def (wadd f O m) in (let TMP_386 \def (eq
496 nat TMP_384 TMP_385) in (let TMP_392 \def (\lambda (x: nat).(\lambda (H6: (eq
497 nat m (S x))).(\lambda (H7: (lt x d)).(let TMP_387 \def (S x) in (let TMP_390
498 \def (\lambda (n: nat).(let TMP_388 \def (wadd g O n) in (let TMP_389 \def
499 (wadd f O n) in (eq nat TMP_388 TMP_389)))) in (let TMP_391 \def (H1 x H7) in
500 (eq_ind_r nat TMP_387 TMP_390 TMP_391 m H6))))))) in (ex2_ind nat TMP_382
501 TMP_383 TMP_386 TMP_392 H5)))))))) in (let TMP_394 \def (lt_gen_xS m d H4) in
502 (or_ind TMP_368 TMP_372 TMP_375 TMP_380 TMP_393 TMP_394))))))))))))) in (let
503 TMP_409 \def (\lambda (m: nat).(\lambda (H4: (le (S d) m)).(let TMP_397 \def
504 (\lambda (n: nat).(let TMP_396 \def (S n) in (eq nat m TMP_396))) in (let
505 TMP_398 \def (\lambda (n: nat).(le d n)) in (let TMP_399 \def (g m) in (let
506 TMP_400 \def (wadd f O m) in (let TMP_401 \def (eq nat TMP_399 TMP_400) in
507 (let TMP_407 \def (\lambda (x: nat).(\lambda (H5: (eq nat m (S x))).(\lambda
508 (H6: (le d x)).(let TMP_402 \def (S x) in (let TMP_405 \def (\lambda (n:
509 nat).(let TMP_403 \def (g n) in (let TMP_404 \def (wadd f O n) in (eq nat
510 TMP_403 TMP_404)))) in (let TMP_406 \def (H3 x H6) in (eq_ind_r nat TMP_402
511 TMP_405 TMP_406 m H5))))))) in (let TMP_408 \def (le_gen_S d m H4) in
512 (ex2_ind nat TMP_397 TMP_398 TMP_401 TMP_407 TMP_408)))))))))) in (let
513 TMP_410 \def (H0 h TMP_365 TMP_366 TMP_367 TMP_395 H2 TMP_409) in (let
514 TMP_411 \def (f_equal2 nat nat nat plus TMP_351 TMP_354 TMP_358 TMP_363
515 TMP_364 TMP_410) in (let TMP_412 \def (f_equal nat nat S TMP_340 TMP_349
516 TMP_411) in (let TMP_413 \def (lift h d t0) in (let TMP_414 \def (weight_map
517 f TMP_413) in (let TMP_415 \def (wadd f O) in (let TMP_416 \def (S d) in (let
518 TMP_417 \def (lift h TMP_416 t1) in (let TMP_418 \def (weight_map TMP_415
519 TMP_417) in (let TMP_419 \def (plus TMP_414 TMP_418) in (let TMP_420 \def (S
520 h) in (let TMP_421 \def (lift TMP_420 d t0) in (let TMP_422 \def (weight_map
521 g TMP_421) in (let TMP_423 \def (wadd g O) in (let TMP_424 \def (S h) in (let
522 TMP_425 \def (S d) in (let TMP_426 \def (lift TMP_424 TMP_425 t1) in (let
523 TMP_427 \def (weight_map TMP_423 TMP_426) in (let TMP_428 \def (plus TMP_422
524 TMP_427) in (let TMP_429 \def (lift h d t0) in (let TMP_430 \def (weight_map
525 f TMP_429) in (let TMP_431 \def (S h) in (let TMP_432 \def (lift TMP_431 d
526 t0) in (let TMP_433 \def (weight_map g TMP_432) in (let TMP_434 \def (wadd f
527 O) in (let TMP_435 \def (S d) in (let TMP_436 \def (lift h TMP_435 t1) in
528 (let TMP_437 \def (weight_map TMP_434 TMP_436) in (let TMP_438 \def (wadd g
529 O) in (let TMP_439 \def (S h) in (let TMP_440 \def (S d) in (let TMP_441 \def
530 (lift TMP_439 TMP_440 t1) in (let TMP_442 \def (weight_map TMP_438 TMP_441)
531 in (let TMP_443 \def (H h d f g H1 H2 H3) in (let TMP_444 \def (S d) in (let
532 TMP_445 \def (wadd f O) in (let TMP_446 \def (wadd g O) in (let TMP_474 \def
533 (\lambda (m: nat).(\lambda (H4: (lt m (S d))).(let TMP_447 \def (eq nat m O)
534 in (let TMP_449 \def (\lambda (m0: nat).(let TMP_448 \def (S m0) in (eq nat m
535 TMP_448))) in (let TMP_450 \def (\lambda (m0: nat).(lt m0 d)) in (let TMP_451
536 \def (ex2 nat TMP_449 TMP_450) in (let TMP_452 \def (wadd g O m) in (let
537 TMP_453 \def (wadd f O m) in (let TMP_454 \def (eq nat TMP_452 TMP_453) in
538 (let TMP_459 \def (\lambda (H5: (eq nat m O)).(let TMP_457 \def (\lambda (n:
539 nat).(let TMP_455 \def (wadd g O n) in (let TMP_456 \def (wadd f O n) in (eq
540 nat TMP_455 TMP_456)))) in (let TMP_458 \def (refl_equal nat O) in (eq_ind_r
541 nat O TMP_457 TMP_458 m H5)))) in (let TMP_472 \def (\lambda (H5: (ex2 nat
542 (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d)))).(let
543 TMP_461 \def (\lambda (m0: nat).(let TMP_460 \def (S m0) in (eq nat m
544 TMP_460))) in (let TMP_462 \def (\lambda (m0: nat).(lt m0 d)) in (let TMP_463
545 \def (wadd g O m) in (let TMP_464 \def (wadd f O m) in (let TMP_465 \def (eq
546 nat TMP_463 TMP_464) in (let TMP_471 \def (\lambda (x: nat).(\lambda (H6: (eq
547 nat m (S x))).(\lambda (H7: (lt x d)).(let TMP_466 \def (S x) in (let TMP_469
548 \def (\lambda (n: nat).(let TMP_467 \def (wadd g O n) in (let TMP_468 \def
549 (wadd f O n) in (eq nat TMP_467 TMP_468)))) in (let TMP_470 \def (H1 x H7) in
550 (eq_ind_r nat TMP_466 TMP_469 TMP_470 m H6))))))) in (ex2_ind nat TMP_461
551 TMP_462 TMP_465 TMP_471 H5)))))))) in (let TMP_473 \def (lt_gen_xS m d H4) in
552 (or_ind TMP_447 TMP_451 TMP_454 TMP_459 TMP_472 TMP_473))))))))))))) in (let
553 TMP_488 \def (\lambda (m: nat).(\lambda (H4: (le (S d) m)).(let TMP_476 \def
554 (\lambda (n: nat).(let TMP_475 \def (S n) in (eq nat m TMP_475))) in (let
555 TMP_477 \def (\lambda (n: nat).(le d n)) in (let TMP_478 \def (g m) in (let
556 TMP_479 \def (wadd f O m) in (let TMP_480 \def (eq nat TMP_478 TMP_479) in
557 (let TMP_486 \def (\lambda (x: nat).(\lambda (H5: (eq nat m (S x))).(\lambda
558 (H6: (le d x)).(let TMP_481 \def (S x) in (let TMP_484 \def (\lambda (n:
559 nat).(let TMP_482 \def (g n) in (let TMP_483 \def (wadd f O n) in (eq nat
560 TMP_482 TMP_483)))) in (let TMP_485 \def (H3 x H6) in (eq_ind_r nat TMP_481
561 TMP_484 TMP_485 m H5))))))) in (let TMP_487 \def (le_gen_S d m H4) in
562 (ex2_ind nat TMP_476 TMP_477 TMP_480 TMP_486 TMP_487)))))))))) in (let
563 TMP_489 \def (H0 h TMP_444 TMP_445 TMP_446 TMP_474 H2 TMP_488) in (let
564 TMP_490 \def (f_equal2 nat nat nat plus TMP_430 TMP_433 TMP_437 TMP_442
565 TMP_443 TMP_489) in (let TMP_491 \def (f_equal nat nat S TMP_419 TMP_428
566 TMP_490) in (let TMP_492 \def (B_ind TMP_187 TMP_333 TMP_412 TMP_491 b) in
567 (let TMP_493 \def (S h) in (let TMP_494 \def (Bind b) in (let TMP_495 \def
568 (THead TMP_494 t0 t1) in (let TMP_496 \def (lift TMP_493 d TMP_495) in (let
569 TMP_497 \def (Bind b) in (let TMP_498 \def (S h) in (let TMP_499 \def
570 (lift_head TMP_497 t0 t1 TMP_498 d) in (let TMP_500 \def (eq_ind_r T TMP_120
571 TMP_129 TMP_492 TMP_496 TMP_499) in (let TMP_501 \def (Bind b) in (let
572 TMP_502 \def (THead TMP_501 t0 t1) in (let TMP_503 \def (lift h d TMP_502) in
573 (let TMP_504 \def (Bind b) in (let TMP_505 \def (lift_head TMP_504 t0 t1 h d)
574 in (eq_ind_r T TMP_105 TMP_112 TMP_500 TMP_503
575 TMP_505)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
576 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
577 )))))))))))))))))))))) in (let TMP_576 \def (\lambda (f0: F).(let TMP_507
578 \def (Flat f0) in (let TMP_508 \def (lift h d t0) in (let TMP_509 \def (Flat
579 f0) in (let TMP_510 \def (s TMP_509 d) in (let TMP_511 \def (lift h TMP_510
580 t1) in (let TMP_512 \def (THead TMP_507 TMP_508 TMP_511) in (let TMP_519 \def
581 (\lambda (t2: T).(let TMP_513 \def (weight_map f t2) in (let TMP_514 \def (S
582 h) in (let TMP_515 \def (Flat f0) in (let TMP_516 \def (THead TMP_515 t0 t1)
583 in (let TMP_517 \def (lift TMP_514 d TMP_516) in (let TMP_518 \def
584 (weight_map g TMP_517) in (eq nat TMP_513 TMP_518)))))))) in (let TMP_520
585 \def (Flat f0) in (let TMP_521 \def (S h) in (let TMP_522 \def (lift TMP_521
586 d t0) in (let TMP_523 \def (S h) in (let TMP_524 \def (Flat f0) in (let
587 TMP_525 \def (s TMP_524 d) in (let TMP_526 \def (lift TMP_523 TMP_525 t1) in
588 (let TMP_527 \def (THead TMP_520 TMP_522 TMP_526) in (let TMP_536 \def
589 (\lambda (t2: T).(let TMP_528 \def (Flat f0) in (let TMP_529 \def (lift h d
590 t0) in (let TMP_530 \def (Flat f0) in (let TMP_531 \def (s TMP_530 d) in (let
591 TMP_532 \def (lift h TMP_531 t1) in (let TMP_533 \def (THead TMP_528 TMP_529
592 TMP_532) in (let TMP_534 \def (weight_map f TMP_533) in (let TMP_535 \def
593 (weight_map g t2) in (eq nat TMP_534 TMP_535)))))))))) in (let TMP_537 \def
594 (lift h d t0) in (let TMP_538 \def (weight_map f TMP_537) in (let TMP_539
595 \def (lift h d t1) in (let TMP_540 \def (weight_map f TMP_539) in (let
596 TMP_541 \def (plus TMP_538 TMP_540) in (let TMP_542 \def (S h) in (let
597 TMP_543 \def (lift TMP_542 d t0) in (let TMP_544 \def (weight_map g TMP_543)
598 in (let TMP_545 \def (S h) in (let TMP_546 \def (lift TMP_545 d t1) in (let
599 TMP_547 \def (weight_map g TMP_546) in (let TMP_548 \def (plus TMP_544
600 TMP_547) in (let TMP_549 \def (lift h d t0) in (let TMP_550 \def (weight_map
601 f TMP_549) in (let TMP_551 \def (S h) in (let TMP_552 \def (lift TMP_551 d
602 t0) in (let TMP_553 \def (weight_map g TMP_552) in (let TMP_554 \def (lift h
603 d t1) in (let TMP_555 \def (weight_map f TMP_554) in (let TMP_556 \def (S h)
604 in (let TMP_557 \def (lift TMP_556 d t1) in (let TMP_558 \def (weight_map g
605 TMP_557) in (let TMP_559 \def (H h d f g H1 H2 H3) in (let TMP_560 \def (H0 h
606 d f g H1 H2 H3) in (let TMP_561 \def (f_equal2 nat nat nat plus TMP_550
607 TMP_553 TMP_555 TMP_558 TMP_559 TMP_560) in (let TMP_562 \def (f_equal nat
608 nat S TMP_541 TMP_548 TMP_561) in (let TMP_563 \def (S h) in (let TMP_564
609 \def (Flat f0) in (let TMP_565 \def (THead TMP_564 t0 t1) in (let TMP_566
610 \def (lift TMP_563 d TMP_565) in (let TMP_567 \def (Flat f0) in (let TMP_568
611 \def (S h) in (let TMP_569 \def (lift_head TMP_567 t0 t1 TMP_568 d) in (let
612 TMP_570 \def (eq_ind_r T TMP_527 TMP_536 TMP_562 TMP_566 TMP_569) in (let
613 TMP_571 \def (Flat f0) in (let TMP_572 \def (THead TMP_571 t0 t1) in (let
614 TMP_573 \def (lift h d TMP_572) in (let TMP_574 \def (Flat f0) in (let
615 TMP_575 \def (lift_head TMP_574 t0 t1 h d) in (eq_ind_r T TMP_512 TMP_519
617 TMP_575))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in (K_ind
618 TMP_99 TMP_506 TMP_576 k)))))))))))))))) in (T_ind TMP_6 TMP_11 TMP_91
621 theorem lift_weight_add_O:
622 \forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (f: ((nat \to
623 nat))).(eq nat (weight_map f (lift h O t)) (weight_map (wadd f w) (lift (S h)
626 \lambda (w: nat).(\lambda (t: T).(\lambda (h: nat).(\lambda (f: ((nat \to
627 nat))).(let TMP_1 \def (wadd f w O) in (let TMP_2 \def (minus TMP_1 O) in
628 (let TMP_3 \def (wadd f w) in (let TMP_7 \def (\lambda (m: nat).(\lambda (H:
629 (lt m O)).(let TMP_4 \def (wadd f w m) in (let TMP_5 \def (f m) in (let TMP_6
630 \def (eq nat TMP_4 TMP_5) in (lt_x_O m H TMP_6)))))) in (let TMP_8 \def (wadd
631 f w O) in (let TMP_9 \def (minus_n_O TMP_8) in (let TMP_11 \def (\lambda (m:
632 nat).(\lambda (_: (le O m)).(let TMP_10 \def (f m) in (refl_equal nat
633 TMP_10)))) in (lift_weight_add TMP_2 t h O f TMP_3 TMP_7 TMP_9
637 \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall
638 (d: nat).(tlt t (THead k u (lift h d t)))))))
640 \lambda (k: K).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda
641 (d: nat).(let TMP_1 \def (lift h d t) in (let TMP_2 \def (weight TMP_1) in
642 (let TMP_6 \def (\lambda (n: nat).(let TMP_3 \def (lift h d t) in (let TMP_4
643 \def (THead k u TMP_3) in (let TMP_5 \def (weight TMP_4) in (lt n TMP_5)))))
644 in (let TMP_7 \def (lift h d t) in (let TMP_8 \def (tlt_head_dx k u TMP_7) in
645 (let TMP_9 \def (weight t) in (let TMP_10 \def (lift_weight t h d) in (eq_ind
646 nat TMP_2 TMP_6 TMP_8 TMP_9 TMP_10)))))))))))).
projects / helm.git / blob