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/pr0/fwd.ma".
19 include "basic_1/subst0/props.ma".
22 \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (h: nat).(\forall
23 (d: nat).(pr0 (lift h d t1) (lift h d t2))))))
25 \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t1 t2)).(let TMP_3 \def
26 (\lambda (t: T).(\lambda (t0: T).(\forall (h: nat).(\forall (d: nat).(let
27 TMP_1 \def (lift h d t) in (let TMP_2 \def (lift h d t0) in (pr0 TMP_1
28 TMP_2))))))) in (let TMP_5 \def (\lambda (t: T).(\lambda (h: nat).(\lambda
29 (d: nat).(let TMP_4 \def (lift h d t) in (pr0_refl TMP_4))))) in (let TMP_39
30 \def (\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda
31 (H1: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d u1) (lift h d
32 u2)))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda
33 (H3: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d t3) (lift h d
34 t4)))))).(\lambda (k: K).(\lambda (h: nat).(\lambda (d: nat).(let TMP_6 \def
35 (lift h d u1) in (let TMP_7 \def (s k d) in (let TMP_8 \def (lift h TMP_7 t3)
36 in (let TMP_9 \def (THead k TMP_6 TMP_8) in (let TMP_12 \def (\lambda (t:
37 T).(let TMP_10 \def (THead k u2 t4) in (let TMP_11 \def (lift h d TMP_10) in
38 (pr0 t TMP_11)))) in (let TMP_13 \def (lift h d u2) in (let TMP_14 \def (s k
39 d) in (let TMP_15 \def (lift h TMP_14 t4) in (let TMP_16 \def (THead k TMP_13
40 TMP_15) in (let TMP_21 \def (\lambda (t: T).(let TMP_17 \def (lift h d u1) in
41 (let TMP_18 \def (s k d) in (let TMP_19 \def (lift h TMP_18 t3) in (let
42 TMP_20 \def (THead k TMP_17 TMP_19) in (pr0 TMP_20 t)))))) in (let TMP_22
43 \def (lift h d u1) in (let TMP_23 \def (lift h d u2) in (let TMP_24 \def (H1
44 h d) in (let TMP_25 \def (s k d) in (let TMP_26 \def (lift h TMP_25 t3) in
45 (let TMP_27 \def (s k d) in (let TMP_28 \def (lift h TMP_27 t4) in (let
46 TMP_29 \def (s k d) in (let TMP_30 \def (H3 h TMP_29) in (let TMP_31 \def
47 (pr0_comp TMP_22 TMP_23 TMP_24 TMP_26 TMP_28 TMP_30 k) in (let TMP_32 \def
48 (THead k u2 t4) in (let TMP_33 \def (lift h d TMP_32) in (let TMP_34 \def
49 (lift_head k u2 t4 h d) in (let TMP_35 \def (eq_ind_r T TMP_16 TMP_21 TMP_31
50 TMP_33 TMP_34) in (let TMP_36 \def (THead k u1 t3) in (let TMP_37 \def (lift
51 h d TMP_36) in (let TMP_38 \def (lift_head k u1 t3 h d) in (eq_ind_r T TMP_9
52 TMP_12 TMP_35 TMP_37 TMP_38))))))))))))))))))))))))))))))))))))))) in (let
53 TMP_132 \def (\lambda (u: T).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_:
54 (pr0 v1 v2)).(\lambda (H1: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h
55 d v1) (lift h d v2)))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0
56 t3 t4)).(\lambda (H3: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d t3)
57 (lift h d t4)))))).(\lambda (h: nat).(\lambda (d: nat).(let TMP_40 \def (Flat
58 Appl) in (let TMP_41 \def (lift h d v1) in (let TMP_42 \def (Flat Appl) in
59 (let TMP_43 \def (s TMP_42 d) in (let TMP_44 \def (Bind Abst) in (let TMP_45
60 \def (THead TMP_44 u t3) in (let TMP_46 \def (lift h TMP_43 TMP_45) in (let
61 TMP_47 \def (THead TMP_40 TMP_41 TMP_46) in (let TMP_51 \def (\lambda (t:
62 T).(let TMP_48 \def (Bind Abbr) in (let TMP_49 \def (THead TMP_48 v2 t4) in
63 (let TMP_50 \def (lift h d TMP_49) in (pr0 t TMP_50))))) in (let TMP_52 \def
64 (Bind Abst) in (let TMP_53 \def (Flat Appl) in (let TMP_54 \def (s TMP_53 d)
65 in (let TMP_55 \def (lift h TMP_54 u) in (let TMP_56 \def (Bind Abst) in (let
66 TMP_57 \def (Flat Appl) in (let TMP_58 \def (s TMP_57 d) in (let TMP_59 \def
67 (s TMP_56 TMP_58) in (let TMP_60 \def (lift h TMP_59 t3) in (let TMP_61 \def
68 (THead TMP_52 TMP_55 TMP_60) in (let TMP_68 \def (\lambda (t: T).(let TMP_62
69 \def (Flat Appl) in (let TMP_63 \def (lift h d v1) in (let TMP_64 \def (THead
70 TMP_62 TMP_63 t) in (let TMP_65 \def (Bind Abbr) in (let TMP_66 \def (THead
71 TMP_65 v2 t4) in (let TMP_67 \def (lift h d TMP_66) in (pr0 TMP_64
72 TMP_67)))))))) in (let TMP_69 \def (Bind Abbr) in (let TMP_70 \def (lift h d
73 v2) in (let TMP_71 \def (Bind Abbr) in (let TMP_72 \def (s TMP_71 d) in (let
74 TMP_73 \def (lift h TMP_72 t4) in (let TMP_74 \def (THead TMP_69 TMP_70
75 TMP_73) in (let TMP_88 \def (\lambda (t: T).(let TMP_75 \def (Flat Appl) in
76 (let TMP_76 \def (lift h d v1) in (let TMP_77 \def (Bind Abst) in (let TMP_78
77 \def (Flat Appl) in (let TMP_79 \def (s TMP_78 d) in (let TMP_80 \def (lift h
78 TMP_79 u) in (let TMP_81 \def (Bind Abst) in (let TMP_82 \def (Flat Appl) in
79 (let TMP_83 \def (s TMP_82 d) in (let TMP_84 \def (s TMP_81 TMP_83) in (let
80 TMP_85 \def (lift h TMP_84 t3) in (let TMP_86 \def (THead TMP_77 TMP_80
81 TMP_85) in (let TMP_87 \def (THead TMP_75 TMP_76 TMP_86) in (pr0 TMP_87
82 t))))))))))))))) in (let TMP_89 \def (Flat Appl) in (let TMP_90 \def (s
83 TMP_89 d) in (let TMP_91 \def (lift h TMP_90 u) in (let TMP_92 \def (lift h d
84 v1) in (let TMP_93 \def (lift h d v2) in (let TMP_94 \def (H1 h d) in (let
85 TMP_95 \def (Bind Abst) in (let TMP_96 \def (Flat Appl) in (let TMP_97 \def
86 (s TMP_96 d) in (let TMP_98 \def (s TMP_95 TMP_97) in (let TMP_99 \def (lift
87 h TMP_98 t3) in (let TMP_100 \def (Bind Abbr) in (let TMP_101 \def (s TMP_100
88 d) in (let TMP_102 \def (lift h TMP_101 t4) in (let TMP_103 \def (Bind Abbr)
89 in (let TMP_104 \def (s TMP_103 d) in (let TMP_105 \def (H3 h TMP_104) in
90 (let TMP_106 \def (pr0_beta TMP_91 TMP_92 TMP_93 TMP_94 TMP_99 TMP_102
91 TMP_105) in (let TMP_107 \def (Bind Abbr) in (let TMP_108 \def (THead TMP_107
92 v2 t4) in (let TMP_109 \def (lift h d TMP_108) in (let TMP_110 \def (Bind
93 Abbr) in (let TMP_111 \def (lift_head TMP_110 v2 t4 h d) in (let TMP_112 \def
94 (eq_ind_r T TMP_74 TMP_88 TMP_106 TMP_109 TMP_111) in (let TMP_113 \def (Flat
95 Appl) in (let TMP_114 \def (s TMP_113 d) in (let TMP_115 \def (Bind Abst) in
96 (let TMP_116 \def (THead TMP_115 u t3) in (let TMP_117 \def (lift h TMP_114
97 TMP_116) in (let TMP_118 \def (Bind Abst) in (let TMP_119 \def (Flat Appl) in
98 (let TMP_120 \def (s TMP_119 d) in (let TMP_121 \def (lift_head TMP_118 u t3
99 h TMP_120) in (let TMP_122 \def (eq_ind_r T TMP_61 TMP_68 TMP_112 TMP_117
100 TMP_121) in (let TMP_123 \def (Flat Appl) in (let TMP_124 \def (Bind Abst) in
101 (let TMP_125 \def (THead TMP_124 u t3) in (let TMP_126 \def (THead TMP_123 v1
102 TMP_125) in (let TMP_127 \def (lift h d TMP_126) in (let TMP_128 \def (Flat
103 Appl) in (let TMP_129 \def (Bind Abst) in (let TMP_130 \def (THead TMP_129 u
104 t3) in (let TMP_131 \def (lift_head TMP_128 v1 TMP_130 h d) in (eq_ind_r T
105 TMP_47 TMP_51 TMP_122 TMP_127
106 TMP_131)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
107 ))))))))))) in (let TMP_339 \def (\lambda (b: B).(\lambda (H0: (not (eq B b
108 Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda
109 (H2: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d v1) (lift h d
110 v2)))))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda
111 (H4: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d u1) (lift h d
112 u2)))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda
113 (H6: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d t3) (lift h d
114 t4)))))).(\lambda (h: nat).(\lambda (d: nat).(let TMP_133 \def (Flat Appl) in
115 (let TMP_134 \def (lift h d v1) in (let TMP_135 \def (Flat Appl) in (let
116 TMP_136 \def (s TMP_135 d) in (let TMP_137 \def (Bind b) in (let TMP_138 \def
117 (THead TMP_137 u1 t3) in (let TMP_139 \def (lift h TMP_136 TMP_138) in (let
118 TMP_140 \def (THead TMP_133 TMP_134 TMP_139) in (let TMP_148 \def (\lambda
119 (t: T).(let TMP_141 \def (Bind b) in (let TMP_142 \def (Flat Appl) in (let
120 TMP_143 \def (S O) in (let TMP_144 \def (lift TMP_143 O v2) in (let TMP_145
121 \def (THead TMP_142 TMP_144 t4) in (let TMP_146 \def (THead TMP_141 u2
122 TMP_145) in (let TMP_147 \def (lift h d TMP_146) in (pr0 t TMP_147)))))))))
123 in (let TMP_149 \def (Bind b) in (let TMP_150 \def (Flat Appl) in (let
124 TMP_151 \def (s TMP_150 d) in (let TMP_152 \def (lift h TMP_151 u1) in (let
125 TMP_153 \def (Bind b) in (let TMP_154 \def (Flat Appl) in (let TMP_155 \def
126 (s TMP_154 d) in (let TMP_156 \def (s TMP_153 TMP_155) in (let TMP_157 \def
127 (lift h TMP_156 t3) in (let TMP_158 \def (THead TMP_149 TMP_152 TMP_157) in
128 (let TMP_169 \def (\lambda (t: T).(let TMP_159 \def (Flat Appl) in (let
129 TMP_160 \def (lift h d v1) in (let TMP_161 \def (THead TMP_159 TMP_160 t) in
130 (let TMP_162 \def (Bind b) in (let TMP_163 \def (Flat Appl) in (let TMP_164
131 \def (S O) in (let TMP_165 \def (lift TMP_164 O v2) in (let TMP_166 \def
132 (THead TMP_163 TMP_165 t4) in (let TMP_167 \def (THead TMP_162 u2 TMP_166) in
133 (let TMP_168 \def (lift h d TMP_167) in (pr0 TMP_161 TMP_168)))))))))))) in
134 (let TMP_170 \def (Bind b) in (let TMP_171 \def (lift h d u2) in (let TMP_172
135 \def (Bind b) in (let TMP_173 \def (s TMP_172 d) in (let TMP_174 \def (Flat
136 Appl) in (let TMP_175 \def (S O) in (let TMP_176 \def (lift TMP_175 O v2) in
137 (let TMP_177 \def (THead TMP_174 TMP_176 t4) in (let TMP_178 \def (lift h
138 TMP_173 TMP_177) in (let TMP_179 \def (THead TMP_170 TMP_171 TMP_178) in (let
139 TMP_193 \def (\lambda (t: T).(let TMP_180 \def (Flat Appl) in (let TMP_181
140 \def (lift h d v1) in (let TMP_182 \def (Bind b) in (let TMP_183 \def (Flat
141 Appl) in (let TMP_184 \def (s TMP_183 d) in (let TMP_185 \def (lift h TMP_184
142 u1) in (let TMP_186 \def (Bind b) in (let TMP_187 \def (Flat Appl) in (let
143 TMP_188 \def (s TMP_187 d) in (let TMP_189 \def (s TMP_186 TMP_188) in (let
144 TMP_190 \def (lift h TMP_189 t3) in (let TMP_191 \def (THead TMP_182 TMP_185
145 TMP_190) in (let TMP_192 \def (THead TMP_180 TMP_181 TMP_191) in (pr0 TMP_192
146 t))))))))))))))) in (let TMP_194 \def (Flat Appl) in (let TMP_195 \def (Bind
147 b) in (let TMP_196 \def (s TMP_195 d) in (let TMP_197 \def (S O) in (let
148 TMP_198 \def (lift TMP_197 O v2) in (let TMP_199 \def (lift h TMP_196
149 TMP_198) in (let TMP_200 \def (Flat Appl) in (let TMP_201 \def (Bind b) in
150 (let TMP_202 \def (s TMP_201 d) in (let TMP_203 \def (s TMP_200 TMP_202) in
151 (let TMP_204 \def (lift h TMP_203 t4) in (let TMP_205 \def (THead TMP_194
152 TMP_199 TMP_204) in (let TMP_222 \def (\lambda (t: T).(let TMP_206 \def (Flat
153 Appl) in (let TMP_207 \def (lift h d v1) in (let TMP_208 \def (Bind b) in
154 (let TMP_209 \def (Flat Appl) in (let TMP_210 \def (s TMP_209 d) in (let
155 TMP_211 \def (lift h TMP_210 u1) in (let TMP_212 \def (Bind b) in (let
156 TMP_213 \def (Flat Appl) in (let TMP_214 \def (s TMP_213 d) in (let TMP_215
157 \def (s TMP_212 TMP_214) in (let TMP_216 \def (lift h TMP_215 t3) in (let
158 TMP_217 \def (THead TMP_208 TMP_211 TMP_216) in (let TMP_218 \def (THead
159 TMP_206 TMP_207 TMP_217) in (let TMP_219 \def (Bind b) in (let TMP_220 \def
160 (lift h d u2) in (let TMP_221 \def (THead TMP_219 TMP_220 t) in (pr0 TMP_218
161 TMP_221)))))))))))))))))) in (let TMP_223 \def (S O) in (let TMP_224 \def
162 (plus TMP_223 d) in (let TMP_241 \def (\lambda (n: nat).(let TMP_225 \def
163 (Flat Appl) in (let TMP_226 \def (lift h d v1) in (let TMP_227 \def (Bind b)
164 in (let TMP_228 \def (lift h d u1) in (let TMP_229 \def (lift h n t3) in (let
165 TMP_230 \def (THead TMP_227 TMP_228 TMP_229) in (let TMP_231 \def (THead
166 TMP_225 TMP_226 TMP_230) in (let TMP_232 \def (Bind b) in (let TMP_233 \def
167 (lift h d u2) in (let TMP_234 \def (Flat Appl) in (let TMP_235 \def (S O) in
168 (let TMP_236 \def (lift TMP_235 O v2) in (let TMP_237 \def (lift h n TMP_236)
169 in (let TMP_238 \def (lift h n t4) in (let TMP_239 \def (THead TMP_234
170 TMP_237 TMP_238) in (let TMP_240 \def (THead TMP_232 TMP_233 TMP_239) in (pr0
171 TMP_231 TMP_240)))))))))))))))))) in (let TMP_242 \def (S O) in (let TMP_243
172 \def (lift h d v2) in (let TMP_244 \def (lift TMP_242 O TMP_243) in (let
173 TMP_262 \def (\lambda (t: T).(let TMP_245 \def (Flat Appl) in (let TMP_246
174 \def (lift h d v1) in (let TMP_247 \def (Bind b) in (let TMP_248 \def (lift h
175 d u1) in (let TMP_249 \def (S O) in (let TMP_250 \def (plus TMP_249 d) in
176 (let TMP_251 \def (lift h TMP_250 t3) in (let TMP_252 \def (THead TMP_247
177 TMP_248 TMP_251) in (let TMP_253 \def (THead TMP_245 TMP_246 TMP_252) in (let
178 TMP_254 \def (Bind b) in (let TMP_255 \def (lift h d u2) in (let TMP_256 \def
179 (Flat Appl) in (let TMP_257 \def (S O) in (let TMP_258 \def (plus TMP_257 d)
180 in (let TMP_259 \def (lift h TMP_258 t4) in (let TMP_260 \def (THead TMP_256
181 t TMP_259) in (let TMP_261 \def (THead TMP_254 TMP_255 TMP_260) in (pr0
182 TMP_253 TMP_261))))))))))))))))))) in (let TMP_263 \def (lift h d v1) in (let
183 TMP_264 \def (lift h d v2) in (let TMP_265 \def (H2 h d) in (let TMP_266 \def
184 (lift h d u1) in (let TMP_267 \def (lift h d u2) in (let TMP_268 \def (H4 h
185 d) in (let TMP_269 \def (S O) in (let TMP_270 \def (plus TMP_269 d) in (let
186 TMP_271 \def (lift h TMP_270 t3) in (let TMP_272 \def (S O) in (let TMP_273
187 \def (plus TMP_272 d) in (let TMP_274 \def (lift h TMP_273 t4) in (let
188 TMP_275 \def (S O) in (let TMP_276 \def (plus TMP_275 d) in (let TMP_277 \def
189 (H6 h TMP_276) in (let TMP_278 \def (pr0_upsilon b H0 TMP_263 TMP_264 TMP_265
190 TMP_266 TMP_267 TMP_268 TMP_271 TMP_274 TMP_277) in (let TMP_279 \def (S O)
191 in (let TMP_280 \def (plus TMP_279 d) in (let TMP_281 \def (S O) in (let
192 TMP_282 \def (lift TMP_281 O v2) in (let TMP_283 \def (lift h TMP_280
193 TMP_282) in (let TMP_284 \def (S O) in (let TMP_285 \def (le_O_n d) in (let
194 TMP_286 \def (lift_d v2 h TMP_284 d O TMP_285) in (let TMP_287 \def (eq_ind_r
195 T TMP_244 TMP_262 TMP_278 TMP_283 TMP_286) in (let TMP_288 \def (S d) in (let
196 TMP_289 \def (S d) in (let TMP_290 \def (refl_equal nat TMP_289) in (let
197 TMP_291 \def (eq_ind nat TMP_224 TMP_241 TMP_287 TMP_288 TMP_290) in (let
198 TMP_292 \def (Bind b) in (let TMP_293 \def (s TMP_292 d) in (let TMP_294 \def
199 (Flat Appl) in (let TMP_295 \def (S O) in (let TMP_296 \def (lift TMP_295 O
200 v2) in (let TMP_297 \def (THead TMP_294 TMP_296 t4) in (let TMP_298 \def
201 (lift h TMP_293 TMP_297) in (let TMP_299 \def (Flat Appl) in (let TMP_300
202 \def (S O) in (let TMP_301 \def (lift TMP_300 O v2) in (let TMP_302 \def
203 (Bind b) in (let TMP_303 \def (s TMP_302 d) in (let TMP_304 \def (lift_head
204 TMP_299 TMP_301 t4 h TMP_303) in (let TMP_305 \def (eq_ind_r T TMP_205
205 TMP_222 TMP_291 TMP_298 TMP_304) in (let TMP_306 \def (Bind b) in (let
206 TMP_307 \def (Flat Appl) in (let TMP_308 \def (S O) in (let TMP_309 \def
207 (lift TMP_308 O v2) in (let TMP_310 \def (THead TMP_307 TMP_309 t4) in (let
208 TMP_311 \def (THead TMP_306 u2 TMP_310) in (let TMP_312 \def (lift h d
209 TMP_311) in (let TMP_313 \def (Bind b) in (let TMP_314 \def (Flat Appl) in
210 (let TMP_315 \def (S O) in (let TMP_316 \def (lift TMP_315 O v2) in (let
211 TMP_317 \def (THead TMP_314 TMP_316 t4) in (let TMP_318 \def (lift_head
212 TMP_313 u2 TMP_317 h d) in (let TMP_319 \def (eq_ind_r T TMP_179 TMP_193
213 TMP_305 TMP_312 TMP_318) in (let TMP_320 \def (Flat Appl) in (let TMP_321
214 \def (s TMP_320 d) in (let TMP_322 \def (Bind b) in (let TMP_323 \def (THead
215 TMP_322 u1 t3) in (let TMP_324 \def (lift h TMP_321 TMP_323) in (let TMP_325
216 \def (Bind b) in (let TMP_326 \def (Flat Appl) in (let TMP_327 \def (s
217 TMP_326 d) in (let TMP_328 \def (lift_head TMP_325 u1 t3 h TMP_327) in (let
218 TMP_329 \def (eq_ind_r T TMP_158 TMP_169 TMP_319 TMP_324 TMP_328) in (let
219 TMP_330 \def (Flat Appl) in (let TMP_331 \def (Bind b) in (let TMP_332 \def
220 (THead TMP_331 u1 t3) in (let TMP_333 \def (THead TMP_330 v1 TMP_332) in (let
221 TMP_334 \def (lift h d TMP_333) in (let TMP_335 \def (Flat Appl) in (let
222 TMP_336 \def (Bind b) in (let TMP_337 \def (THead TMP_336 u1 t3) in (let
223 TMP_338 \def (lift_head TMP_335 v1 TMP_337 h d) in (eq_ind_r T TMP_140
224 TMP_148 TMP_329 TMP_334
225 TMP_338)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
226 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in
227 (let TMP_405 \def (\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1
228 u2)).(\lambda (H1: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d u1)
229 (lift h d u2)))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3
230 t4)).(\lambda (H3: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d t3)
231 (lift h d t4)))))).(\lambda (w: T).(\lambda (H4: (subst0 O u2 t4 w)).(\lambda
232 (h: nat).(\lambda (d: nat).(let TMP_340 \def (Bind Abbr) in (let TMP_341 \def
233 (lift h d u1) in (let TMP_342 \def (Bind Abbr) in (let TMP_343 \def (s
234 TMP_342 d) in (let TMP_344 \def (lift h TMP_343 t3) in (let TMP_345 \def
235 (THead TMP_340 TMP_341 TMP_344) in (let TMP_349 \def (\lambda (t: T).(let
236 TMP_346 \def (Bind Abbr) in (let TMP_347 \def (THead TMP_346 u2 w) in (let
237 TMP_348 \def (lift h d TMP_347) in (pr0 t TMP_348))))) in (let TMP_350 \def
238 (Bind Abbr) in (let TMP_351 \def (lift h d u2) in (let TMP_352 \def (Bind
239 Abbr) in (let TMP_353 \def (s TMP_352 d) in (let TMP_354 \def (lift h TMP_353
240 w) in (let TMP_355 \def (THead TMP_350 TMP_351 TMP_354) in (let TMP_362 \def
241 (\lambda (t: T).(let TMP_356 \def (Bind Abbr) in (let TMP_357 \def (lift h d
242 u1) in (let TMP_358 \def (Bind Abbr) in (let TMP_359 \def (s TMP_358 d) in
243 (let TMP_360 \def (lift h TMP_359 t3) in (let TMP_361 \def (THead TMP_356
244 TMP_357 TMP_360) in (pr0 TMP_361 t)))))))) in (let TMP_363 \def (lift h d u1)
245 in (let TMP_364 \def (lift h d u2) in (let TMP_365 \def (H1 h d) in (let
246 TMP_366 \def (S d) in (let TMP_367 \def (lift h TMP_366 t3) in (let TMP_368
247 \def (S d) in (let TMP_369 \def (lift h TMP_368 t4) in (let TMP_370 \def (S
248 d) in (let TMP_371 \def (H3 h TMP_370) in (let TMP_372 \def (S d) in (let
249 TMP_373 \def (lift h TMP_372 w) in (let d' \def (S d) in (let TMP_374 \def (S
250 d) in (let TMP_375 \def (S O) in (let TMP_376 \def (minus TMP_374 TMP_375) in
251 (let TMP_380 \def (\lambda (n: nat).(let TMP_377 \def (lift h n u2) in (let
252 TMP_378 \def (lift h d' t4) in (let TMP_379 \def (lift h d' w) in (subst0 O
253 TMP_377 TMP_378 TMP_379))))) in (let TMP_381 \def (S d) in (let TMP_382 \def
254 (le_O_n d) in (let TMP_383 \def (le_n_S O d TMP_382) in (let TMP_384 \def
255 (subst0_lift_lt t4 w u2 O H4 TMP_381 TMP_383 h) in (let TMP_385 \def (\lambda
256 (n: nat).(eq nat n d)) in (let TMP_386 \def (le_n d) in (let TMP_387 \def
257 (le_n d) in (let TMP_388 \def (le_antisym d d TMP_386 TMP_387) in (let
258 TMP_389 \def (minus d O) in (let TMP_390 \def (minus_n_O d) in (let TMP_391
259 \def (eq_ind nat d TMP_385 TMP_388 TMP_389 TMP_390) in (let TMP_392 \def
260 (eq_ind nat TMP_376 TMP_380 TMP_384 d TMP_391) in (let TMP_393 \def
261 (pr0_delta TMP_363 TMP_364 TMP_365 TMP_367 TMP_369 TMP_371 TMP_373 TMP_392)
262 in (let TMP_394 \def (Bind Abbr) in (let TMP_395 \def (THead TMP_394 u2 w) in
263 (let TMP_396 \def (lift h d TMP_395) in (let TMP_397 \def (Bind Abbr) in (let
264 TMP_398 \def (lift_head TMP_397 u2 w h d) in (let TMP_399 \def (eq_ind_r T
265 TMP_355 TMP_362 TMP_393 TMP_396 TMP_398) in (let TMP_400 \def (Bind Abbr) in
266 (let TMP_401 \def (THead TMP_400 u1 t3) in (let TMP_402 \def (lift h d
267 TMP_401) in (let TMP_403 \def (Bind Abbr) in (let TMP_404 \def (lift_head
268 TMP_403 u1 t3 h d) in (eq_ind_r T TMP_345 TMP_349 TMP_399 TMP_402
269 TMP_404))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in
270 (let TMP_461 \def (\lambda (b: B).(\lambda (H0: (not (eq B b Abst))).(\lambda
271 (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda (H2: ((\forall
272 (h: nat).(\forall (d: nat).(pr0 (lift h d t3) (lift h d t4)))))).(\lambda (u:
273 T).(\lambda (h: nat).(\lambda (d: nat).(let TMP_406 \def (Bind b) in (let
274 TMP_407 \def (lift h d u) in (let TMP_408 \def (Bind b) in (let TMP_409 \def
275 (s TMP_408 d) in (let TMP_410 \def (S O) in (let TMP_411 \def (lift TMP_410 O
276 t3) in (let TMP_412 \def (lift h TMP_409 TMP_411) in (let TMP_413 \def (THead
277 TMP_406 TMP_407 TMP_412) in (let TMP_415 \def (\lambda (t: T).(let TMP_414
278 \def (lift h d t4) in (pr0 t TMP_414))) in (let TMP_416 \def (S O) in (let
279 TMP_417 \def (plus TMP_416 d) in (let TMP_425 \def (\lambda (n: nat).(let
280 TMP_418 \def (Bind b) in (let TMP_419 \def (lift h d u) in (let TMP_420 \def
281 (S O) in (let TMP_421 \def (lift TMP_420 O t3) in (let TMP_422 \def (lift h n
282 TMP_421) in (let TMP_423 \def (THead TMP_418 TMP_419 TMP_422) in (let TMP_424
283 \def (lift h d t4) in (pr0 TMP_423 TMP_424))))))))) in (let TMP_426 \def (S
284 O) in (let TMP_427 \def (lift h d t3) in (let TMP_428 \def (lift TMP_426 O
285 TMP_427) in (let TMP_433 \def (\lambda (t: T).(let TMP_429 \def (Bind b) in
286 (let TMP_430 \def (lift h d u) in (let TMP_431 \def (THead TMP_429 TMP_430 t)
287 in (let TMP_432 \def (lift h d t4) in (pr0 TMP_431 TMP_432)))))) in (let
288 TMP_434 \def (lift h d t3) in (let TMP_435 \def (lift h d t4) in (let TMP_436
289 \def (H2 h d) in (let TMP_437 \def (lift h d u) in (let TMP_438 \def
290 (pr0_zeta b H0 TMP_434 TMP_435 TMP_436 TMP_437) in (let TMP_439 \def (S O) in
291 (let TMP_440 \def (plus TMP_439 d) in (let TMP_441 \def (S O) in (let TMP_442
292 \def (lift TMP_441 O t3) in (let TMP_443 \def (lift h TMP_440 TMP_442) in
293 (let TMP_444 \def (S O) in (let TMP_445 \def (le_O_n d) in (let TMP_446 \def
294 (lift_d t3 h TMP_444 d O TMP_445) in (let TMP_447 \def (eq_ind_r T TMP_428
295 TMP_433 TMP_438 TMP_443 TMP_446) in (let TMP_448 \def (S d) in (let TMP_449
296 \def (S d) in (let TMP_450 \def (refl_equal nat TMP_449) in (let TMP_451 \def
297 (eq_ind nat TMP_417 TMP_425 TMP_447 TMP_448 TMP_450) in (let TMP_452 \def
298 (Bind b) in (let TMP_453 \def (S O) in (let TMP_454 \def (lift TMP_453 O t3)
299 in (let TMP_455 \def (THead TMP_452 u TMP_454) in (let TMP_456 \def (lift h d
300 TMP_455) in (let TMP_457 \def (Bind b) in (let TMP_458 \def (S O) in (let
301 TMP_459 \def (lift TMP_458 O t3) in (let TMP_460 \def (lift_head TMP_457 u
302 TMP_459 h d) in (eq_ind_r T TMP_413 TMP_415 TMP_451 TMP_456
303 TMP_460))))))))))))))))))))))))))))))))))))))))))))))))))))) in (let TMP_482
304 \def (\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda
305 (H1: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d t3) (lift h d
306 t4)))))).(\lambda (u: T).(\lambda (h: nat).(\lambda (d: nat).(let TMP_462
307 \def (Flat Cast) in (let TMP_463 \def (lift h d u) in (let TMP_464 \def (Flat
308 Cast) in (let TMP_465 \def (s TMP_464 d) in (let TMP_466 \def (lift h TMP_465
309 t3) in (let TMP_467 \def (THead TMP_462 TMP_463 TMP_466) in (let TMP_469 \def
310 (\lambda (t: T).(let TMP_468 \def (lift h d t4) in (pr0 t TMP_468))) in (let
311 TMP_470 \def (Flat Cast) in (let TMP_471 \def (s TMP_470 d) in (let TMP_472
312 \def (lift h TMP_471 t3) in (let TMP_473 \def (lift h d t4) in (let TMP_474
313 \def (H1 h d) in (let TMP_475 \def (lift h d u) in (let TMP_476 \def (pr0_tau
314 TMP_472 TMP_473 TMP_474 TMP_475) in (let TMP_477 \def (Flat Cast) in (let
315 TMP_478 \def (THead TMP_477 u t3) in (let TMP_479 \def (lift h d TMP_478) in
316 (let TMP_480 \def (Flat Cast) in (let TMP_481 \def (lift_head TMP_480 u t3 h
317 d) in (eq_ind_r T TMP_467 TMP_469 TMP_476 TMP_479
318 TMP_481))))))))))))))))))))))))))) in (pr0_ind TMP_3 TMP_5 TMP_39 TMP_132
319 TMP_339 TMP_405 TMP_461 TMP_482 t1 t2 H))))))))))).
321 theorem pr0_gen_abbr:
322 \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Bind Abbr) u1
323 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead
324 (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
325 (u2: T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T (\lambda (y: T).(pr0 t1 y))
326 (\lambda (y: T).(subst0 O u2 y t2))))))) (pr0 t1 (lift (S O) O x))))))
328 \lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (H: (pr0 (THead
329 (Bind Abbr) u1 t1) x)).(let TMP_1 \def (Bind Abbr) in (let TMP_2 \def (THead
330 TMP_1 u1 t1) in (let TMP_3 \def (\lambda (t: T).(pr0 t x)) in (let TMP_17
331 \def (\lambda (_: T).(let TMP_6 \def (\lambda (u2: T).(\lambda (t2: T).(let
332 TMP_4 \def (Bind Abbr) in (let TMP_5 \def (THead TMP_4 u2 t2) in (eq T x
333 TMP_5))))) in (let TMP_7 \def (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))
334 in (let TMP_12 \def (\lambda (u2: T).(\lambda (t2: T).(let TMP_8 \def (pr0 t1
335 t2) in (let TMP_9 \def (\lambda (y: T).(pr0 t1 y)) in (let TMP_10 \def
336 (\lambda (y: T).(subst0 O u2 y t2)) in (let TMP_11 \def (ex2 T TMP_9 TMP_10)
337 in (or TMP_8 TMP_11))))))) in (let TMP_13 \def (ex3_2 T T TMP_6 TMP_7 TMP_12)
338 in (let TMP_14 \def (S O) in (let TMP_15 \def (lift TMP_14 O x) in (let
339 TMP_16 \def (pr0 t1 TMP_15) in (or TMP_13 TMP_16))))))))) in (let TMP_448
340 \def (\lambda (y: T).(\lambda (H0: (pr0 y x)).(let TMP_31 \def (\lambda (t:
341 T).(\lambda (t0: T).((eq T t (THead (Bind Abbr) u1 t1)) \to (let TMP_20 \def
342 (\lambda (u2: T).(\lambda (t2: T).(let TMP_18 \def (Bind Abbr) in (let TMP_19
343 \def (THead TMP_18 u2 t2) in (eq T t0 TMP_19))))) in (let TMP_21 \def
344 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) in (let TMP_26 \def (\lambda
345 (u2: T).(\lambda (t2: T).(let TMP_22 \def (pr0 t1 t2) in (let TMP_23 \def
346 (\lambda (y0: T).(pr0 t1 y0)) in (let TMP_24 \def (\lambda (y0: T).(subst0 O
347 u2 y0 t2)) in (let TMP_25 \def (ex2 T TMP_23 TMP_24) in (or TMP_22
348 TMP_25))))))) in (let TMP_27 \def (ex3_2 T T TMP_20 TMP_21 TMP_26) in (let
349 TMP_28 \def (S O) in (let TMP_29 \def (lift TMP_28 O t0) in (let TMP_30 \def
350 (pr0 t1 TMP_29) in (or TMP_27 TMP_30))))))))))) in (let TMP_91 \def (\lambda
351 (t: T).(\lambda (H1: (eq T t (THead (Bind Abbr) u1 t1))).(let TMP_32 \def
352 (\lambda (e: T).e) in (let TMP_33 \def (Bind Abbr) in (let TMP_34 \def (THead
353 TMP_33 u1 t1) in (let H2 \def (f_equal T T TMP_32 t TMP_34 H1) in (let TMP_35
354 \def (Bind Abbr) in (let TMP_36 \def (THead TMP_35 u1 t1) in (let TMP_50 \def
355 (\lambda (t0: T).(let TMP_39 \def (\lambda (u2: T).(\lambda (t2: T).(let
356 TMP_37 \def (Bind Abbr) in (let TMP_38 \def (THead TMP_37 u2 t2) in (eq T t0
357 TMP_38))))) in (let TMP_40 \def (\lambda (u2: T).(\lambda (_: T).(pr0 u1
358 u2))) in (let TMP_45 \def (\lambda (u2: T).(\lambda (t2: T).(let TMP_41 \def
359 (pr0 t1 t2) in (let TMP_42 \def (\lambda (y0: T).(pr0 t1 y0)) in (let TMP_43
360 \def (\lambda (y0: T).(subst0 O u2 y0 t2)) in (let TMP_44 \def (ex2 T TMP_42
361 TMP_43) in (or TMP_41 TMP_44))))))) in (let TMP_46 \def (ex3_2 T T TMP_39
362 TMP_40 TMP_45) in (let TMP_47 \def (S O) in (let TMP_48 \def (lift TMP_47 O
363 t0) in (let TMP_49 \def (pr0 t1 TMP_48) in (or TMP_46 TMP_49))))))))) in (let
364 TMP_55 \def (\lambda (u2: T).(\lambda (t2: T).(let TMP_51 \def (Bind Abbr) in
365 (let TMP_52 \def (THead TMP_51 u1 t1) in (let TMP_53 \def (Bind Abbr) in (let
366 TMP_54 \def (THead TMP_53 u2 t2) in (eq T TMP_52 TMP_54))))))) in (let TMP_56
367 \def (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) in (let TMP_61 \def
368 (\lambda (u2: T).(\lambda (t2: T).(let TMP_57 \def (pr0 t1 t2) in (let TMP_58
369 \def (\lambda (y0: T).(pr0 t1 y0)) in (let TMP_59 \def (\lambda (y0:
370 T).(subst0 O u2 y0 t2)) in (let TMP_60 \def (ex2 T TMP_58 TMP_59) in (or
371 TMP_57 TMP_60))))))) in (let TMP_62 \def (ex3_2 T T TMP_55 TMP_56 TMP_61) in
372 (let TMP_63 \def (S O) in (let TMP_64 \def (Bind Abbr) in (let TMP_65 \def
373 (THead TMP_64 u1 t1) in (let TMP_66 \def (lift TMP_63 O TMP_65) in (let
374 TMP_67 \def (pr0 t1 TMP_66) in (let TMP_72 \def (\lambda (u2: T).(\lambda
375 (t2: T).(let TMP_68 \def (Bind Abbr) in (let TMP_69 \def (THead TMP_68 u1 t1)
376 in (let TMP_70 \def (Bind Abbr) in (let TMP_71 \def (THead TMP_70 u2 t2) in
377 (eq T TMP_69 TMP_71))))))) in (let TMP_73 \def (\lambda (u2: T).(\lambda (_:
378 T).(pr0 u1 u2))) in (let TMP_78 \def (\lambda (u2: T).(\lambda (t2: T).(let
379 TMP_74 \def (pr0 t1 t2) in (let TMP_75 \def (\lambda (y0: T).(pr0 t1 y0)) in
380 (let TMP_76 \def (\lambda (y0: T).(subst0 O u2 y0 t2)) in (let TMP_77 \def
381 (ex2 T TMP_75 TMP_76) in (or TMP_74 TMP_77))))))) in (let TMP_79 \def (Bind
382 Abbr) in (let TMP_80 \def (THead TMP_79 u1 t1) in (let TMP_81 \def
383 (refl_equal T TMP_80) in (let TMP_82 \def (pr0_refl u1) in (let TMP_83 \def
384 (pr0 t1 t1) in (let TMP_84 \def (\lambda (y0: T).(pr0 t1 y0)) in (let TMP_85
385 \def (\lambda (y0: T).(subst0 O u1 y0 t1)) in (let TMP_86 \def (ex2 T TMP_84
386 TMP_85) in (let TMP_87 \def (pr0_refl t1) in (let TMP_88 \def (or_introl
387 TMP_83 TMP_86 TMP_87) in (let TMP_89 \def (ex3_2_intro T T TMP_72 TMP_73
388 TMP_78 u1 t1 TMP_81 TMP_82 TMP_88) in (let TMP_90 \def (or_introl TMP_62
389 TMP_67 TMP_89) in (eq_ind_r T TMP_36 TMP_50 TMP_90 t
390 H2)))))))))))))))))))))))))))))))))) in (let TMP_191 \def (\lambda (u0:
391 T).(\lambda (u2: T).(\lambda (H1: (pr0 u0 u2)).(\lambda (H2: (((eq T u0
392 (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2:
393 T).(eq T u2 (THead (Bind Abbr) u3 t2)))) (\lambda (u3: T).(\lambda (_:
394 T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T
395 (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u3 y0 t2))))))) (pr0
396 t1 (lift (S O) O u2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H3:
397 (pr0 t0 t2)).(\lambda (H4: (((eq T t0 (THead (Bind Abbr) u1 t1)) \to (or
398 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u3
399 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3:
400 T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
401 (\lambda (y0: T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O
402 t2)))))).(\lambda (k: K).(\lambda (H5: (eq T (THead k u0 t0) (THead (Bind
403 Abbr) u1 t1))).(let TMP_92 \def (\lambda (e: T).(match e with [(TSort _)
404 \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) in
405 (let TMP_93 \def (THead k u0 t0) in (let TMP_94 \def (Bind Abbr) in (let
406 TMP_95 \def (THead TMP_94 u1 t1) in (let H6 \def (f_equal T K TMP_92 TMP_93
407 TMP_95 H5) in (let TMP_96 \def (\lambda (e: T).(match e with [(TSort _)
408 \Rightarrow u0 | (TLRef _) \Rightarrow u0 | (THead _ t _) \Rightarrow t])) in
409 (let TMP_97 \def (THead k u0 t0) in (let TMP_98 \def (Bind Abbr) in (let
410 TMP_99 \def (THead TMP_98 u1 t1) in (let H7 \def (f_equal T T TMP_96 TMP_97
411 TMP_99 H5) in (let TMP_100 \def (\lambda (e: T).(match e with [(TSort _)
412 \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) in
413 (let TMP_101 \def (THead k u0 t0) in (let TMP_102 \def (Bind Abbr) in (let
414 TMP_103 \def (THead TMP_102 u1 t1) in (let H8 \def (f_equal T T TMP_100
415 TMP_101 TMP_103 H5) in (let TMP_189 \def (\lambda (H9: (eq T u0 u1)).(\lambda
416 (H10: (eq K k (Bind Abbr))).(let TMP_104 \def (Bind Abbr) in (let TMP_120
417 \def (\lambda (k0: K).(let TMP_108 \def (\lambda (u3: T).(\lambda (t3:
418 T).(let TMP_105 \def (THead k0 u2 t2) in (let TMP_106 \def (Bind Abbr) in
419 (let TMP_107 \def (THead TMP_106 u3 t3) in (eq T TMP_105 TMP_107)))))) in
420 (let TMP_109 \def (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) in (let
421 TMP_114 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_110 \def (pr0 t1 t3)
422 in (let TMP_111 \def (\lambda (y0: T).(pr0 t1 y0)) in (let TMP_112 \def
423 (\lambda (y0: T).(subst0 O u3 y0 t3)) in (let TMP_113 \def (ex2 T TMP_111
424 TMP_112) in (or TMP_110 TMP_113))))))) in (let TMP_115 \def (ex3_2 T T
425 TMP_108 TMP_109 TMP_114) in (let TMP_116 \def (S O) in (let TMP_117 \def
426 (THead k0 u2 t2) in (let TMP_118 \def (lift TMP_116 O TMP_117) in (let
427 TMP_119 \def (pr0 t1 TMP_118) in (or TMP_115 TMP_119)))))))))) in (let
428 TMP_134 \def (\lambda (t: T).((eq T t (THead (Bind Abbr) u1 t1)) \to (let
429 TMP_123 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_121 \def (Bind Abbr)
430 in (let TMP_122 \def (THead TMP_121 u3 t3) in (eq T t2 TMP_122))))) in (let
431 TMP_124 \def (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) in (let TMP_129
432 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_125 \def (pr0 t1 t3) in (let
433 TMP_126 \def (\lambda (y0: T).(pr0 t1 y0)) in (let TMP_127 \def (\lambda (y0:
434 T).(subst0 O u3 y0 t3)) in (let TMP_128 \def (ex2 T TMP_126 TMP_127) in (or
435 TMP_125 TMP_128))))))) in (let TMP_130 \def (ex3_2 T T TMP_123 TMP_124
436 TMP_129) in (let TMP_131 \def (S O) in (let TMP_132 \def (lift TMP_131 O t2)
437 in (let TMP_133 \def (pr0 t1 TMP_132) in (or TMP_130 TMP_133)))))))))) in
438 (let H11 \def (eq_ind T t0 TMP_134 H4 t1 H8) in (let TMP_135 \def (\lambda
439 (t: T).(pr0 t t2)) in (let H12 \def (eq_ind T t0 TMP_135 H3 t1 H8) in (let
440 TMP_149 \def (\lambda (t: T).((eq T t (THead (Bind Abbr) u1 t1)) \to (let
441 TMP_138 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_136 \def (Bind Abbr)
442 in (let TMP_137 \def (THead TMP_136 u3 t3) in (eq T u2 TMP_137))))) in (let
443 TMP_139 \def (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) in (let TMP_144
444 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_140 \def (pr0 t1 t3) in (let
445 TMP_141 \def (\lambda (y0: T).(pr0 t1 y0)) in (let TMP_142 \def (\lambda (y0:
446 T).(subst0 O u3 y0 t3)) in (let TMP_143 \def (ex2 T TMP_141 TMP_142) in (or
447 TMP_140 TMP_143))))))) in (let TMP_145 \def (ex3_2 T T TMP_138 TMP_139
448 TMP_144) in (let TMP_146 \def (S O) in (let TMP_147 \def (lift TMP_146 O u2)
449 in (let TMP_148 \def (pr0 t1 TMP_147) in (or TMP_145 TMP_148)))))))))) in
450 (let H13 \def (eq_ind T u0 TMP_149 H2 u1 H9) in (let TMP_150 \def (\lambda
451 (t: T).(pr0 t u2)) in (let H14 \def (eq_ind T u0 TMP_150 H1 u1 H9) in (let
452 TMP_155 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_151 \def (Bind Abbr)
453 in (let TMP_152 \def (THead TMP_151 u2 t2) in (let TMP_153 \def (Bind Abbr)
454 in (let TMP_154 \def (THead TMP_153 u3 t3) in (eq T TMP_152 TMP_154))))))) in
455 (let TMP_156 \def (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) in (let
456 TMP_161 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_157 \def (pr0 t1 t3)
457 in (let TMP_158 \def (\lambda (y0: T).(pr0 t1 y0)) in (let TMP_159 \def
458 (\lambda (y0: T).(subst0 O u3 y0 t3)) in (let TMP_160 \def (ex2 T TMP_158
459 TMP_159) in (or TMP_157 TMP_160))))))) in (let TMP_162 \def (ex3_2 T T
460 TMP_155 TMP_156 TMP_161) in (let TMP_163 \def (S O) in (let TMP_164 \def
461 (Bind Abbr) in (let TMP_165 \def (THead TMP_164 u2 t2) in (let TMP_166 \def
462 (lift TMP_163 O TMP_165) in (let TMP_167 \def (pr0 t1 TMP_166) in (let
463 TMP_172 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_168 \def (Bind Abbr)
464 in (let TMP_169 \def (THead TMP_168 u2 t2) in (let TMP_170 \def (Bind Abbr)
465 in (let TMP_171 \def (THead TMP_170 u3 t3) in (eq T TMP_169 TMP_171))))))) in
466 (let TMP_173 \def (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) in (let
467 TMP_178 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_174 \def (pr0 t1 t3)
468 in (let TMP_175 \def (\lambda (y0: T).(pr0 t1 y0)) in (let TMP_176 \def
469 (\lambda (y0: T).(subst0 O u3 y0 t3)) in (let TMP_177 \def (ex2 T TMP_175
470 TMP_176) in (or TMP_174 TMP_177))))))) in (let TMP_179 \def (Bind Abbr) in
471 (let TMP_180 \def (THead TMP_179 u2 t2) in (let TMP_181 \def (refl_equal T
472 TMP_180) in (let TMP_182 \def (pr0 t1 t2) in (let TMP_183 \def (\lambda (y0:
473 T).(pr0 t1 y0)) in (let TMP_184 \def (\lambda (y0: T).(subst0 O u2 y0 t2)) in
474 (let TMP_185 \def (ex2 T TMP_183 TMP_184) in (let TMP_186 \def (or_introl
475 TMP_182 TMP_185 H12) in (let TMP_187 \def (ex3_2_intro T T TMP_172 TMP_173
476 TMP_178 u2 t2 TMP_181 H14 TMP_186) in (let TMP_188 \def (or_introl TMP_162
477 TMP_167 TMP_187) in (eq_ind_r K TMP_104 TMP_120 TMP_188 k
478 H10))))))))))))))))))))))))))))))))))) in (let TMP_190 \def (TMP_189 H7) in
479 (TMP_190 H6)))))))))))))))))))))))))))) in (let TMP_217 \def (\lambda (u:
480 T).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_:
481 (((eq T v1 (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u2:
482 T).(\lambda (t2: T).(eq T v2 (THead (Bind Abbr) u2 t2)))) (\lambda (u2:
483 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: T).(\lambda (t2: T).(or (pr0
484 t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u2 y0
485 t2))))))) (pr0 t1 (lift (S O) O v2)))))).(\lambda (t0: T).(\lambda (t2:
486 T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind Abbr) u1
487 t1)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead
488 (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
489 (u2: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
490 (\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t1 (lift (S O) O
491 t2)))))).(\lambda (H5: (eq T (THead (Flat Appl) v1 (THead (Bind Abst) u t0))
492 (THead (Bind Abbr) u1 t1))).(let TMP_192 \def (Flat Appl) in (let TMP_193
493 \def (Bind Abst) in (let TMP_194 \def (THead TMP_193 u t0) in (let TMP_195
494 \def (THead TMP_192 v1 TMP_194) in (let TMP_196 \def (\lambda (ee: T).(match
495 ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k
496 _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat _)
497 \Rightarrow True])])) in (let TMP_197 \def (Bind Abbr) in (let TMP_198 \def
498 (THead TMP_197 u1 t1) in (let H6 \def (eq_ind T TMP_195 TMP_196 I TMP_198 H5)
499 in (let TMP_203 \def (\lambda (u2: T).(\lambda (t3: T).(let TMP_199 \def
500 (Bind Abbr) in (let TMP_200 \def (THead TMP_199 v2 t2) in (let TMP_201 \def
501 (Bind Abbr) in (let TMP_202 \def (THead TMP_201 u2 t3) in (eq T TMP_200
502 TMP_202))))))) in (let TMP_204 \def (\lambda (u2: T).(\lambda (_: T).(pr0 u1
503 u2))) in (let TMP_209 \def (\lambda (u2: T).(\lambda (t3: T).(let TMP_205
504 \def (pr0 t1 t3) in (let TMP_206 \def (\lambda (y0: T).(pr0 t1 y0)) in (let
505 TMP_207 \def (\lambda (y0: T).(subst0 O u2 y0 t3)) in (let TMP_208 \def (ex2
506 T TMP_206 TMP_207) in (or TMP_205 TMP_208))))))) in (let TMP_210 \def (ex3_2
507 T T TMP_203 TMP_204 TMP_209) in (let TMP_211 \def (S O) in (let TMP_212 \def
508 (Bind Abbr) in (let TMP_213 \def (THead TMP_212 v2 t2) in (let TMP_214 \def
509 (lift TMP_211 O TMP_213) in (let TMP_215 \def (pr0 t1 TMP_214) in (let
510 TMP_216 \def (or TMP_210 TMP_215) in (False_ind TMP_216
511 H6))))))))))))))))))))))))))))) in (let TMP_251 \def (\lambda (b: B).(\lambda
512 (_: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0
513 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T
514 (\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Bind Abbr) u2 t2))))
515 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: T).(\lambda (t2:
516 T).(or (pr0 t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0:
517 T).(subst0 O u2 y0 t2))))))) (pr0 t1 (lift (S O) O v2)))))).(\lambda (u0:
518 T).(\lambda (u2: T).(\lambda (_: (pr0 u0 u2)).(\lambda (_: (((eq T u0 (THead
519 (Bind Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq
520 T u2 (THead (Bind Abbr) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1
521 u3))) (\lambda (u3: T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T (\lambda (y0:
522 T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u3 y0 t2))))))) (pr0 t1 (lift (S
523 O) O u2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0
524 t2)).(\lambda (_: (((eq T t0 (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T
525 (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u3 t3))))
526 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t3:
527 T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0:
528 T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (H8: (eq
529 T (THead (Flat Appl) v1 (THead (Bind b) u0 t0)) (THead (Bind Abbr) u1
530 t1))).(let TMP_218 \def (Flat Appl) in (let TMP_219 \def (Bind b) in (let
531 TMP_220 \def (THead TMP_219 u0 t0) in (let TMP_221 \def (THead TMP_218 v1
532 TMP_220) in (let TMP_222 \def (\lambda (ee: T).(match ee with [(TSort _)
533 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
534 (match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) in
535 (let TMP_223 \def (Bind Abbr) in (let TMP_224 \def (THead TMP_223 u1 t1) in
536 (let H9 \def (eq_ind T TMP_221 TMP_222 I TMP_224 H8) in (let TMP_233 \def
537 (\lambda (u3: T).(\lambda (t3: T).(let TMP_225 \def (Bind b) in (let TMP_226
538 \def (Flat Appl) in (let TMP_227 \def (S O) in (let TMP_228 \def (lift
539 TMP_227 O v2) in (let TMP_229 \def (THead TMP_226 TMP_228 t2) in (let TMP_230
540 \def (THead TMP_225 u2 TMP_229) in (let TMP_231 \def (Bind Abbr) in (let
541 TMP_232 \def (THead TMP_231 u3 t3) in (eq T TMP_230 TMP_232))))))))))) in
542 (let TMP_234 \def (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) in (let
543 TMP_239 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_235 \def (pr0 t1 t3)
544 in (let TMP_236 \def (\lambda (y0: T).(pr0 t1 y0)) in (let TMP_237 \def
545 (\lambda (y0: T).(subst0 O u3 y0 t3)) in (let TMP_238 \def (ex2 T TMP_236
546 TMP_237) in (or TMP_235 TMP_238))))))) in (let TMP_240 \def (ex3_2 T T
547 TMP_233 TMP_234 TMP_239) in (let TMP_241 \def (S O) in (let TMP_242 \def
548 (Bind b) in (let TMP_243 \def (Flat Appl) in (let TMP_244 \def (S O) in (let
549 TMP_245 \def (lift TMP_244 O v2) in (let TMP_246 \def (THead TMP_243 TMP_245
550 t2) in (let TMP_247 \def (THead TMP_242 u2 TMP_246) in (let TMP_248 \def
551 (lift TMP_241 O TMP_247) in (let TMP_249 \def (pr0 t1 TMP_248) in (let
552 TMP_250 \def (or TMP_240 TMP_249) in (False_ind TMP_250
553 H9)))))))))))))))))))))))))))))))))))))) in (let TMP_333 \def (\lambda (u0:
554 T).(\lambda (u2: T).(\lambda (H1: (pr0 u0 u2)).(\lambda (H2: (((eq T u0
555 (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2:
556 T).(eq T u2 (THead (Bind Abbr) u3 t2)))) (\lambda (u3: T).(\lambda (_:
557 T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T
558 (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u3 y0 t2))))))) (pr0
559 t1 (lift (S O) O u2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H3:
560 (pr0 t0 t2)).(\lambda (H4: (((eq T t0 (THead (Bind Abbr) u1 t1)) \to (or
561 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u3
562 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3:
563 T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
564 (\lambda (y0: T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O
565 t2)))))).(\lambda (w: T).(\lambda (H5: (subst0 O u2 t2 w)).(\lambda (H6: (eq
566 T (THead (Bind Abbr) u0 t0) (THead (Bind Abbr) u1 t1))).(let TMP_252 \def
567 (\lambda (e: T).(match e with [(TSort _) \Rightarrow u0 | (TLRef _)
568 \Rightarrow u0 | (THead _ t _) \Rightarrow t])) in (let TMP_253 \def (Bind
569 Abbr) in (let TMP_254 \def (THead TMP_253 u0 t0) in (let TMP_255 \def (Bind
570 Abbr) in (let TMP_256 \def (THead TMP_255 u1 t1) in (let H7 \def (f_equal T T
571 TMP_252 TMP_254 TMP_256 H6) in (let TMP_257 \def (\lambda (e: T).(match e
572 with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t)
573 \Rightarrow t])) in (let TMP_258 \def (Bind Abbr) in (let TMP_259 \def (THead
574 TMP_258 u0 t0) in (let TMP_260 \def (Bind Abbr) in (let TMP_261 \def (THead
575 TMP_260 u1 t1) in (let H8 \def (f_equal T T TMP_257 TMP_259 TMP_261 H6) in
576 (let TMP_332 \def (\lambda (H9: (eq T u0 u1)).(let TMP_275 \def (\lambda (t:
577 T).((eq T t (THead (Bind Abbr) u1 t1)) \to (let TMP_264 \def (\lambda (u3:
578 T).(\lambda (t3: T).(let TMP_262 \def (Bind Abbr) in (let TMP_263 \def (THead
579 TMP_262 u3 t3) in (eq T t2 TMP_263))))) in (let TMP_265 \def (\lambda (u3:
580 T).(\lambda (_: T).(pr0 u1 u3))) in (let TMP_270 \def (\lambda (u3:
581 T).(\lambda (t3: T).(let TMP_266 \def (pr0 t1 t3) in (let TMP_267 \def
582 (\lambda (y0: T).(pr0 t1 y0)) in (let TMP_268 \def (\lambda (y0: T).(subst0 O
583 u3 y0 t3)) in (let TMP_269 \def (ex2 T TMP_267 TMP_268) in (or TMP_266
584 TMP_269))))))) in (let TMP_271 \def (ex3_2 T T TMP_264 TMP_265 TMP_270) in
585 (let TMP_272 \def (S O) in (let TMP_273 \def (lift TMP_272 O t2) in (let
586 TMP_274 \def (pr0 t1 TMP_273) in (or TMP_271 TMP_274)))))))))) in (let H10
587 \def (eq_ind T t0 TMP_275 H4 t1 H8) in (let TMP_276 \def (\lambda (t: T).(pr0
588 t t2)) in (let H11 \def (eq_ind T t0 TMP_276 H3 t1 H8) in (let TMP_290 \def
589 (\lambda (t: T).((eq T t (THead (Bind Abbr) u1 t1)) \to (let TMP_279 \def
590 (\lambda (u3: T).(\lambda (t3: T).(let TMP_277 \def (Bind Abbr) in (let
591 TMP_278 \def (THead TMP_277 u3 t3) in (eq T u2 TMP_278))))) in (let TMP_280
592 \def (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) in (let TMP_285 \def
593 (\lambda (u3: T).(\lambda (t3: T).(let TMP_281 \def (pr0 t1 t3) in (let
594 TMP_282 \def (\lambda (y0: T).(pr0 t1 y0)) in (let TMP_283 \def (\lambda (y0:
595 T).(subst0 O u3 y0 t3)) in (let TMP_284 \def (ex2 T TMP_282 TMP_283) in (or
596 TMP_281 TMP_284))))))) in (let TMP_286 \def (ex3_2 T T TMP_279 TMP_280
597 TMP_285) in (let TMP_287 \def (S O) in (let TMP_288 \def (lift TMP_287 O u2)
598 in (let TMP_289 \def (pr0 t1 TMP_288) in (or TMP_286 TMP_289)))))))))) in
599 (let H12 \def (eq_ind T u0 TMP_290 H2 u1 H9) in (let TMP_291 \def (\lambda
600 (t: T).(pr0 t u2)) in (let H13 \def (eq_ind T u0 TMP_291 H1 u1 H9) in (let
601 TMP_296 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_292 \def (Bind Abbr)
602 in (let TMP_293 \def (THead TMP_292 u2 w) in (let TMP_294 \def (Bind Abbr) in
603 (let TMP_295 \def (THead TMP_294 u3 t3) in (eq T TMP_293 TMP_295))))))) in
604 (let TMP_297 \def (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) in (let
605 TMP_302 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_298 \def (pr0 t1 t3)
606 in (let TMP_299 \def (\lambda (y0: T).(pr0 t1 y0)) in (let TMP_300 \def
607 (\lambda (y0: T).(subst0 O u3 y0 t3)) in (let TMP_301 \def (ex2 T TMP_299
608 TMP_300) in (or TMP_298 TMP_301))))))) in (let TMP_303 \def (ex3_2 T T
609 TMP_296 TMP_297 TMP_302) in (let TMP_304 \def (S O) in (let TMP_305 \def
610 (Bind Abbr) in (let TMP_306 \def (THead TMP_305 u2 w) in (let TMP_307 \def
611 (lift TMP_304 O TMP_306) in (let TMP_308 \def (pr0 t1 TMP_307) in (let
612 TMP_313 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_309 \def (Bind Abbr)
613 in (let TMP_310 \def (THead TMP_309 u2 w) in (let TMP_311 \def (Bind Abbr) in
614 (let TMP_312 \def (THead TMP_311 u3 t3) in (eq T TMP_310 TMP_312))))))) in
615 (let TMP_314 \def (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) in (let
616 TMP_319 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_315 \def (pr0 t1 t3)
617 in (let TMP_316 \def (\lambda (y0: T).(pr0 t1 y0)) in (let TMP_317 \def
618 (\lambda (y0: T).(subst0 O u3 y0 t3)) in (let TMP_318 \def (ex2 T TMP_316
619 TMP_317) in (or TMP_315 TMP_318))))))) in (let TMP_320 \def (Bind Abbr) in
620 (let TMP_321 \def (THead TMP_320 u2 w) in (let TMP_322 \def (refl_equal T
621 TMP_321) in (let TMP_323 \def (pr0 t1 w) in (let TMP_324 \def (\lambda (y0:
622 T).(pr0 t1 y0)) in (let TMP_325 \def (\lambda (y0: T).(subst0 O u2 y0 w)) in
623 (let TMP_326 \def (ex2 T TMP_324 TMP_325) in (let TMP_327 \def (\lambda (y0:
624 T).(pr0 t1 y0)) in (let TMP_328 \def (\lambda (y0: T).(subst0 O u2 y0 w)) in
625 (let TMP_329 \def (ex_intro2 T TMP_327 TMP_328 t2 H11 H5) in (let TMP_330
626 \def (or_intror TMP_323 TMP_326 TMP_329) in (let TMP_331 \def (ex3_2_intro T
627 T TMP_313 TMP_314 TMP_319 u2 w TMP_322 H13 TMP_330) in (or_introl TMP_303
628 TMP_308 TMP_331)))))))))))))))))))))))))))))))))) in (TMP_332
629 H7))))))))))))))))))))))))) in (let TMP_427 \def (\lambda (b: B).(\lambda
630 (H1: (not (eq B b Abst))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H2:
631 (pr0 t0 t2)).(\lambda (H3: (((eq T t0 (THead (Bind Abbr) u1 t1)) \to (or
632 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2
633 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2:
634 T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
635 (\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t1 (lift (S O) O
636 t2)))))).(\lambda (u: T).(\lambda (H4: (eq T (THead (Bind b) u (lift (S O) O
637 t0)) (THead (Bind Abbr) u1 t1))).(let TMP_334 \def (\lambda (e: T).(match e
638 with [(TSort _) \Rightarrow b | (TLRef _) \Rightarrow b | (THead k _ _)
639 \Rightarrow (match k with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow
640 b])])) in (let TMP_335 \def (Bind b) in (let TMP_336 \def (S O) in (let
641 TMP_337 \def (lift TMP_336 O t0) in (let TMP_338 \def (THead TMP_335 u
642 TMP_337) in (let TMP_339 \def (Bind Abbr) in (let TMP_340 \def (THead TMP_339
643 u1 t1) in (let H5 \def (f_equal T B TMP_334 TMP_338 TMP_340 H4) in (let
644 TMP_341 \def (\lambda (e: T).(match e with [(TSort _) \Rightarrow u | (TLRef
645 _) \Rightarrow u | (THead _ t _) \Rightarrow t])) in (let TMP_342 \def (Bind
646 b) in (let TMP_343 \def (S O) in (let TMP_344 \def (lift TMP_343 O t0) in
647 (let TMP_345 \def (THead TMP_342 u TMP_344) in (let TMP_346 \def (Bind Abbr)
648 in (let TMP_347 \def (THead TMP_346 u1 t1) in (let H6 \def (f_equal T T
649 TMP_341 TMP_345 TMP_347 H4) in (let TMP_362 \def (\lambda (e: T).(match e
650 with [(TSort _) \Rightarrow (let TMP_361 \def (\lambda (x0: nat).(let TMP_360
651 \def (S O) in (plus x0 TMP_360))) in (lref_map TMP_361 O t0)) | (TLRef _)
652 \Rightarrow (let TMP_354 \def (\lambda (x0: nat).(let TMP_353 \def (S O) in
653 (plus x0 TMP_353))) in (lref_map TMP_354 O t0)) | (THead _ _ t) \Rightarrow
654 t])) in (let TMP_363 \def (Bind b) in (let TMP_364 \def (S O) in (let TMP_365
655 \def (lift TMP_364 O t0) in (let TMP_366 \def (THead TMP_363 u TMP_365) in
656 (let TMP_367 \def (Bind Abbr) in (let TMP_368 \def (THead TMP_367 u1 t1) in
657 (let H7 \def (f_equal T T TMP_362 TMP_366 TMP_368 H4) in (let TMP_425 \def
658 (\lambda (_: (eq T u u1)).(\lambda (H9: (eq B b Abbr)).(let TMP_370 \def
659 (\lambda (b0: B).(let TMP_369 \def (eq B b0 Abst) in (not TMP_369))) in (let
660 H10 \def (eq_ind B b TMP_370 H1 Abbr H9) in (let TMP_384 \def (\lambda (t:
661 T).((eq T t0 (THead (Bind Abbr) u1 t)) \to (let TMP_373 \def (\lambda (u2:
662 T).(\lambda (t3: T).(let TMP_371 \def (Bind Abbr) in (let TMP_372 \def (THead
663 TMP_371 u2 t3) in (eq T t2 TMP_372))))) in (let TMP_374 \def (\lambda (u2:
664 T).(\lambda (_: T).(pr0 u1 u2))) in (let TMP_379 \def (\lambda (u2:
665 T).(\lambda (t3: T).(let TMP_375 \def (pr0 t t3) in (let TMP_376 \def
666 (\lambda (y0: T).(pr0 t y0)) in (let TMP_377 \def (\lambda (y0: T).(subst0 O
667 u2 y0 t3)) in (let TMP_378 \def (ex2 T TMP_376 TMP_377) in (or TMP_375
668 TMP_378))))))) in (let TMP_380 \def (ex3_2 T T TMP_373 TMP_374 TMP_379) in
669 (let TMP_381 \def (S O) in (let TMP_382 \def (lift TMP_381 O t2) in (let
670 TMP_383 \def (pr0 t TMP_382) in (or TMP_380 TMP_383)))))))))) in (let TMP_385
671 \def (S O) in (let TMP_386 \def (lift TMP_385 O t0) in (let H11 \def
672 (eq_ind_r T t1 TMP_384 H3 TMP_386 H7) in (let TMP_387 \def (S O) in (let
673 TMP_388 \def (lift TMP_387 O t0) in (let TMP_402 \def (\lambda (t: T).(let
674 TMP_391 \def (\lambda (u2: T).(\lambda (t3: T).(let TMP_389 \def (Bind Abbr)
675 in (let TMP_390 \def (THead TMP_389 u2 t3) in (eq T t2 TMP_390))))) in (let
676 TMP_392 \def (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) in (let TMP_397
677 \def (\lambda (u2: T).(\lambda (t3: T).(let TMP_393 \def (pr0 t t3) in (let
678 TMP_394 \def (\lambda (y0: T).(pr0 t y0)) in (let TMP_395 \def (\lambda (y0:
679 T).(subst0 O u2 y0 t3)) in (let TMP_396 \def (ex2 T TMP_394 TMP_395) in (or
680 TMP_393 TMP_396))))))) in (let TMP_398 \def (ex3_2 T T TMP_391 TMP_392
681 TMP_397) in (let TMP_399 \def (S O) in (let TMP_400 \def (lift TMP_399 O t2)
682 in (let TMP_401 \def (pr0 t TMP_400) in (or TMP_398 TMP_401))))))))) in (let
683 TMP_405 \def (\lambda (u2: T).(\lambda (t3: T).(let TMP_403 \def (Bind Abbr)
684 in (let TMP_404 \def (THead TMP_403 u2 t3) in (eq T t2 TMP_404))))) in (let
685 TMP_406 \def (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) in (let TMP_415
686 \def (\lambda (u2: T).(\lambda (t3: T).(let TMP_407 \def (S O) in (let
687 TMP_408 \def (lift TMP_407 O t0) in (let TMP_409 \def (pr0 TMP_408 t3) in
688 (let TMP_412 \def (\lambda (y0: T).(let TMP_410 \def (S O) in (let TMP_411
689 \def (lift TMP_410 O t0) in (pr0 TMP_411 y0)))) in (let TMP_413 \def (\lambda
690 (y0: T).(subst0 O u2 y0 t3)) in (let TMP_414 \def (ex2 T TMP_412 TMP_413) in
691 (or TMP_409 TMP_414))))))))) in (let TMP_416 \def (ex3_2 T T TMP_405 TMP_406
692 TMP_415) in (let TMP_417 \def (S O) in (let TMP_418 \def (lift TMP_417 O t0)
693 in (let TMP_419 \def (S O) in (let TMP_420 \def (lift TMP_419 O t2) in (let
694 TMP_421 \def (pr0 TMP_418 TMP_420) in (let TMP_422 \def (S O) in (let TMP_423
695 \def (pr0_lift t0 t2 H2 TMP_422 O) in (let TMP_424 \def (or_intror TMP_416
696 TMP_421 TMP_423) in (eq_ind T TMP_388 TMP_402 TMP_424 t1
697 H7)))))))))))))))))))))))) in (let TMP_426 \def (TMP_425 H6) in (TMP_426
698 H5))))))))))))))))))))))))))))))))))) in (let TMP_447 \def (\lambda (t0:
699 T).(\lambda (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead
700 (Bind Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq
701 T t2 (THead (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1
702 u2))) (\lambda (u2: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0:
703 T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t1 (lift (S
704 O) O t2)))))).(\lambda (u: T).(\lambda (H3: (eq T (THead (Flat Cast) u t0)
705 (THead (Bind Abbr) u1 t1))).(let TMP_428 \def (Flat Cast) in (let TMP_429
706 \def (THead TMP_428 u t0) in (let TMP_430 \def (\lambda (ee: T).(match ee
707 with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _
708 _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat _)
709 \Rightarrow True])])) in (let TMP_431 \def (Bind Abbr) in (let TMP_432 \def
710 (THead TMP_431 u1 t1) in (let H4 \def (eq_ind T TMP_429 TMP_430 I TMP_432 H3)
711 in (let TMP_435 \def (\lambda (u2: T).(\lambda (t3: T).(let TMP_433 \def
712 (Bind Abbr) in (let TMP_434 \def (THead TMP_433 u2 t3) in (eq T t2
713 TMP_434))))) in (let TMP_436 \def (\lambda (u2: T).(\lambda (_: T).(pr0 u1
714 u2))) in (let TMP_441 \def (\lambda (u2: T).(\lambda (t3: T).(let TMP_437
715 \def (pr0 t1 t3) in (let TMP_438 \def (\lambda (y0: T).(pr0 t1 y0)) in (let
716 TMP_439 \def (\lambda (y0: T).(subst0 O u2 y0 t3)) in (let TMP_440 \def (ex2
717 T TMP_438 TMP_439) in (or TMP_437 TMP_440))))))) in (let TMP_442 \def (ex3_2
718 T T TMP_435 TMP_436 TMP_441) in (let TMP_443 \def (S O) in (let TMP_444 \def
719 (lift TMP_443 O t2) in (let TMP_445 \def (pr0 t1 TMP_444) in (let TMP_446
720 \def (or TMP_442 TMP_445) in (False_ind TMP_446 H4))))))))))))))))))))) in
721 (pr0_ind TMP_31 TMP_91 TMP_191 TMP_217 TMP_251 TMP_333 TMP_427 TMP_447 y x
722 H0))))))))))) in (insert_eq T TMP_2 TMP_3 TMP_17 TMP_448 H))))))))).
724 theorem pr0_gen_void:
725 \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Bind Void) u1
726 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead
727 (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
728 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O x))))))
730 \lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (H: (pr0 (THead
731 (Bind Void) u1 t1) x)).(let TMP_1 \def (Bind Void) in (let TMP_2 \def (THead
732 TMP_1 u1 t1) in (let TMP_3 \def (\lambda (t: T).(pr0 t x)) in (let TMP_13
733 \def (\lambda (_: T).(let TMP_6 \def (\lambda (u2: T).(\lambda (t2: T).(let
734 TMP_4 \def (Bind Void) in (let TMP_5 \def (THead TMP_4 u2 t2) in (eq T x
735 TMP_5))))) in (let TMP_7 \def (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))
736 in (let TMP_8 \def (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2))) in (let
737 TMP_9 \def (ex3_2 T T TMP_6 TMP_7 TMP_8) in (let TMP_10 \def (S O) in (let
738 TMP_11 \def (lift TMP_10 O x) in (let TMP_12 \def (pr0 t1 TMP_11) in (or
739 TMP_9 TMP_12))))))))) in (let TMP_310 \def (\lambda (y: T).(\lambda (H0: (pr0
740 y x)).(let TMP_23 \def (\lambda (t: T).(\lambda (t0: T).((eq T t (THead (Bind
741 Void) u1 t1)) \to (let TMP_16 \def (\lambda (u2: T).(\lambda (t2: T).(let
742 TMP_14 \def (Bind Void) in (let TMP_15 \def (THead TMP_14 u2 t2) in (eq T t0
743 TMP_15))))) in (let TMP_17 \def (\lambda (u2: T).(\lambda (_: T).(pr0 u1
744 u2))) in (let TMP_18 \def (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2))) in
745 (let TMP_19 \def (ex3_2 T T TMP_16 TMP_17 TMP_18) in (let TMP_20 \def (S O)
746 in (let TMP_21 \def (lift TMP_20 O t0) in (let TMP_22 \def (pr0 t1 TMP_21) in
747 (or TMP_19 TMP_22))))))))))) in (let TMP_66 \def (\lambda (t: T).(\lambda
748 (H1: (eq T t (THead (Bind Void) u1 t1))).(let TMP_24 \def (\lambda (e: T).e)
749 in (let TMP_25 \def (Bind Void) in (let TMP_26 \def (THead TMP_25 u1 t1) in
750 (let H2 \def (f_equal T T TMP_24 t TMP_26 H1) in (let TMP_27 \def (Bind Void)
751 in (let TMP_28 \def (THead TMP_27 u1 t1) in (let TMP_38 \def (\lambda (t0:
752 T).(let TMP_31 \def (\lambda (u2: T).(\lambda (t2: T).(let TMP_29 \def (Bind
753 Void) in (let TMP_30 \def (THead TMP_29 u2 t2) in (eq T t0 TMP_30))))) in
754 (let TMP_32 \def (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) in (let
755 TMP_33 \def (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2))) in (let TMP_34
756 \def (ex3_2 T T TMP_31 TMP_32 TMP_33) in (let TMP_35 \def (S O) in (let
757 TMP_36 \def (lift TMP_35 O t0) in (let TMP_37 \def (pr0 t1 TMP_36) in (or
758 TMP_34 TMP_37))))))))) in (let TMP_43 \def (\lambda (u2: T).(\lambda (t2:
759 T).(let TMP_39 \def (Bind Void) in (let TMP_40 \def (THead TMP_39 u1 t1) in
760 (let TMP_41 \def (Bind Void) in (let TMP_42 \def (THead TMP_41 u2 t2) in (eq
761 T TMP_40 TMP_42))))))) in (let TMP_44 \def (\lambda (u2: T).(\lambda (_:
762 T).(pr0 u1 u2))) in (let TMP_45 \def (\lambda (_: T).(\lambda (t2: T).(pr0 t1
763 t2))) in (let TMP_46 \def (ex3_2 T T TMP_43 TMP_44 TMP_45) in (let TMP_47
764 \def (S O) in (let TMP_48 \def (Bind Void) in (let TMP_49 \def (THead TMP_48
765 u1 t1) in (let TMP_50 \def (lift TMP_47 O TMP_49) in (let TMP_51 \def (pr0 t1
766 TMP_50) in (let TMP_56 \def (\lambda (u2: T).(\lambda (t2: T).(let TMP_52
767 \def (Bind Void) in (let TMP_53 \def (THead TMP_52 u1 t1) in (let TMP_54 \def
768 (Bind Void) in (let TMP_55 \def (THead TMP_54 u2 t2) in (eq T TMP_53
769 TMP_55))))))) in (let TMP_57 \def (\lambda (u2: T).(\lambda (_: T).(pr0 u1
770 u2))) in (let TMP_58 \def (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2))) in
771 (let TMP_59 \def (Bind Void) in (let TMP_60 \def (THead TMP_59 u1 t1) in (let
772 TMP_61 \def (refl_equal T TMP_60) in (let TMP_62 \def (pr0_refl u1) in (let
773 TMP_63 \def (pr0_refl t1) in (let TMP_64 \def (ex3_2_intro T T TMP_56 TMP_57
774 TMP_58 u1 t1 TMP_61 TMP_62 TMP_63) in (let TMP_65 \def (or_introl TMP_46
775 TMP_51 TMP_64) in (eq_ind_r T TMP_28 TMP_38 TMP_65 t
776 H2))))))))))))))))))))))))))))) in (let TMP_141 \def (\lambda (u0:
777 T).(\lambda (u2: T).(\lambda (H1: (pr0 u0 u2)).(\lambda (H2: (((eq T u0
778 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2:
779 T).(eq T u2 (THead (Bind Void) u3 t2)))) (\lambda (u3: T).(\lambda (_:
780 T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1
781 (lift (S O) O u2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H3: (pr0
782 t0 t2)).(\lambda (H4: (((eq T t0 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T
783 T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u3 t3))))
784 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
785 T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (k: K).(\lambda
786 (H5: (eq T (THead k u0 t0) (THead (Bind Void) u1 t1))).(let TMP_67 \def
787 (\lambda (e: T).(match e with [(TSort _) \Rightarrow k | (TLRef _)
788 \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) in (let TMP_68 \def (THead k
789 u0 t0) in (let TMP_69 \def (Bind Void) in (let TMP_70 \def (THead TMP_69 u1
790 t1) in (let H6 \def (f_equal T K TMP_67 TMP_68 TMP_70 H5) in (let TMP_71 \def
791 (\lambda (e: T).(match e with [(TSort _) \Rightarrow u0 | (TLRef _)
792 \Rightarrow u0 | (THead _ t _) \Rightarrow t])) in (let TMP_72 \def (THead k
793 u0 t0) in (let TMP_73 \def (Bind Void) in (let TMP_74 \def (THead TMP_73 u1
794 t1) in (let H7 \def (f_equal T T TMP_71 TMP_72 TMP_74 H5) in (let TMP_75 \def
795 (\lambda (e: T).(match e with [(TSort _) \Rightarrow t0 | (TLRef _)
796 \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) in (let TMP_76 \def (THead k
797 u0 t0) in (let TMP_77 \def (Bind Void) in (let TMP_78 \def (THead TMP_77 u1
798 t1) in (let H8 \def (f_equal T T TMP_75 TMP_76 TMP_78 H5) in (let TMP_139
799 \def (\lambda (H9: (eq T u0 u1)).(\lambda (H10: (eq K k (Bind Void))).(let
800 TMP_79 \def (Bind Void) in (let TMP_91 \def (\lambda (k0: K).(let TMP_83 \def
801 (\lambda (u3: T).(\lambda (t3: T).(let TMP_80 \def (THead k0 u2 t2) in (let
802 TMP_81 \def (Bind Void) in (let TMP_82 \def (THead TMP_81 u3 t3) in (eq T
803 TMP_80 TMP_82)))))) in (let TMP_84 \def (\lambda (u3: T).(\lambda (_: T).(pr0
804 u1 u3))) in (let TMP_85 \def (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))
805 in (let TMP_86 \def (ex3_2 T T TMP_83 TMP_84 TMP_85) in (let TMP_87 \def (S
806 O) in (let TMP_88 \def (THead k0 u2 t2) in (let TMP_89 \def (lift TMP_87 O
807 TMP_88) in (let TMP_90 \def (pr0 t1 TMP_89) in (or TMP_86 TMP_90)))))))))) in
808 (let TMP_101 \def (\lambda (t: T).((eq T t (THead (Bind Void) u1 t1)) \to
809 (let TMP_94 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_92 \def (Bind
810 Void) in (let TMP_93 \def (THead TMP_92 u3 t3) in (eq T t2 TMP_93))))) in
811 (let TMP_95 \def (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) in (let
812 TMP_96 \def (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3))) in (let TMP_97
813 \def (ex3_2 T T TMP_94 TMP_95 TMP_96) in (let TMP_98 \def (S O) in (let
814 TMP_99 \def (lift TMP_98 O t2) in (let TMP_100 \def (pr0 t1 TMP_99) in (or
815 TMP_97 TMP_100)))))))))) in (let H11 \def (eq_ind T t0 TMP_101 H4 t1 H8) in
816 (let TMP_102 \def (\lambda (t: T).(pr0 t t2)) in (let H12 \def (eq_ind T t0
817 TMP_102 H3 t1 H8) in (let TMP_112 \def (\lambda (t: T).((eq T t (THead (Bind
818 Void) u1 t1)) \to (let TMP_105 \def (\lambda (u3: T).(\lambda (t3: T).(let
819 TMP_103 \def (Bind Void) in (let TMP_104 \def (THead TMP_103 u3 t3) in (eq T
820 u2 TMP_104))))) in (let TMP_106 \def (\lambda (u3: T).(\lambda (_: T).(pr0 u1
821 u3))) in (let TMP_107 \def (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3))) in
822 (let TMP_108 \def (ex3_2 T T TMP_105 TMP_106 TMP_107) in (let TMP_109 \def (S
823 O) in (let TMP_110 \def (lift TMP_109 O u2) in (let TMP_111 \def (pr0 t1
824 TMP_110) in (or TMP_108 TMP_111)))))))))) in (let H13 \def (eq_ind T u0
825 TMP_112 H2 u1 H9) in (let TMP_113 \def (\lambda (t: T).(pr0 t u2)) in (let
826 H14 \def (eq_ind T u0 TMP_113 H1 u1 H9) in (let TMP_118 \def (\lambda (u3:
827 T).(\lambda (t3: T).(let TMP_114 \def (Bind Void) in (let TMP_115 \def (THead
828 TMP_114 u2 t2) in (let TMP_116 \def (Bind Void) in (let TMP_117 \def (THead
829 TMP_116 u3 t3) in (eq T TMP_115 TMP_117))))))) in (let TMP_119 \def (\lambda
830 (u3: T).(\lambda (_: T).(pr0 u1 u3))) in (let TMP_120 \def (\lambda (_:
831 T).(\lambda (t3: T).(pr0 t1 t3))) in (let TMP_121 \def (ex3_2 T T TMP_118
832 TMP_119 TMP_120) in (let TMP_122 \def (S O) in (let TMP_123 \def (Bind Void)
833 in (let TMP_124 \def (THead TMP_123 u2 t2) in (let TMP_125 \def (lift TMP_122
834 O TMP_124) in (let TMP_126 \def (pr0 t1 TMP_125) in (let TMP_131 \def
835 (\lambda (u3: T).(\lambda (t3: T).(let TMP_127 \def (Bind Void) in (let
836 TMP_128 \def (THead TMP_127 u2 t2) in (let TMP_129 \def (Bind Void) in (let
837 TMP_130 \def (THead TMP_129 u3 t3) in (eq T TMP_128 TMP_130))))))) in (let
838 TMP_132 \def (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) in (let TMP_133
839 \def (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3))) in (let TMP_134 \def
840 (Bind Void) in (let TMP_135 \def (THead TMP_134 u2 t2) in (let TMP_136 \def
841 (refl_equal T TMP_135) in (let TMP_137 \def (ex3_2_intro T T TMP_131 TMP_132
842 TMP_133 u2 t2 TMP_136 H14 H12) in (let TMP_138 \def (or_introl TMP_121
843 TMP_126 TMP_137) in (eq_ind_r K TMP_79 TMP_91 TMP_138 k
844 H10)))))))))))))))))))))))))))))) in (let TMP_140 \def (TMP_139 H7) in
845 (TMP_140 H6)))))))))))))))))))))))))))) in (let TMP_163 \def (\lambda (u:
846 T).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_:
847 (((eq T v1 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T (\lambda (u2:
848 T).(\lambda (t2: T).(eq T v2 (THead (Bind Void) u2 t2)))) (\lambda (u2:
849 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1
850 t2)))) (pr0 t1 (lift (S O) O v2)))))).(\lambda (t0: T).(\lambda (t2:
851 T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind Void) u1
852 t1)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead
853 (Bind Void) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
854 (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O
855 t2)))))).(\lambda (H5: (eq T (THead (Flat Appl) v1 (THead (Bind Abst) u t0))
856 (THead (Bind Void) u1 t1))).(let TMP_142 \def (Flat Appl) in (let TMP_143
857 \def (Bind Abst) in (let TMP_144 \def (THead TMP_143 u t0) in (let TMP_145
858 \def (THead TMP_142 v1 TMP_144) in (let TMP_146 \def (\lambda (ee: T).(match
859 ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k
860 _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat _)
861 \Rightarrow True])])) in (let TMP_147 \def (Bind Void) in (let TMP_148 \def
862 (THead TMP_147 u1 t1) in (let H6 \def (eq_ind T TMP_145 TMP_146 I TMP_148 H5)
863 in (let TMP_153 \def (\lambda (u2: T).(\lambda (t3: T).(let TMP_149 \def
864 (Bind Abbr) in (let TMP_150 \def (THead TMP_149 v2 t2) in (let TMP_151 \def
865 (Bind Void) in (let TMP_152 \def (THead TMP_151 u2 t3) in (eq T TMP_150
866 TMP_152))))))) in (let TMP_154 \def (\lambda (u2: T).(\lambda (_: T).(pr0 u1
867 u2))) in (let TMP_155 \def (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3))) in
868 (let TMP_156 \def (ex3_2 T T TMP_153 TMP_154 TMP_155) in (let TMP_157 \def (S
869 O) in (let TMP_158 \def (Bind Abbr) in (let TMP_159 \def (THead TMP_158 v2
870 t2) in (let TMP_160 \def (lift TMP_157 O TMP_159) in (let TMP_161 \def (pr0
871 t1 TMP_160) in (let TMP_162 \def (or TMP_156 TMP_161) in (False_ind TMP_162
872 H6))))))))))))))))))))))))))))) in (let TMP_193 \def (\lambda (b: B).(\lambda
873 (_: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0
874 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T
875 (\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Bind Void) u2 t2))))
876 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2:
877 T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O v2)))))).(\lambda (u0: T).(\lambda
878 (u2: T).(\lambda (_: (pr0 u0 u2)).(\lambda (_: (((eq T u0 (THead (Bind Void)
879 u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead
880 (Bind Void) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
881 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O
882 u2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda
883 (_: (((eq T t0 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T (\lambda (u3:
884 T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u3 t3)))) (\lambda (u3:
885 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
886 t3)))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (H8: (eq T (THead (Flat Appl)
887 v1 (THead (Bind b) u0 t0)) (THead (Bind Void) u1 t1))).(let TMP_164 \def
888 (Flat Appl) in (let TMP_165 \def (Bind b) in (let TMP_166 \def (THead TMP_165
889 u0 t0) in (let TMP_167 \def (THead TMP_164 v1 TMP_166) in (let TMP_168 \def
890 (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
891 \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _)
892 \Rightarrow False | (Flat _) \Rightarrow True])])) in (let TMP_169 \def (Bind
893 Void) in (let TMP_170 \def (THead TMP_169 u1 t1) in (let H9 \def (eq_ind T
894 TMP_167 TMP_168 I TMP_170 H8) in (let TMP_179 \def (\lambda (u3: T).(\lambda
895 (t3: T).(let TMP_171 \def (Bind b) in (let TMP_172 \def (Flat Appl) in (let
896 TMP_173 \def (S O) in (let TMP_174 \def (lift TMP_173 O v2) in (let TMP_175
897 \def (THead TMP_172 TMP_174 t2) in (let TMP_176 \def (THead TMP_171 u2
898 TMP_175) in (let TMP_177 \def (Bind Void) in (let TMP_178 \def (THead TMP_177
899 u3 t3) in (eq T TMP_176 TMP_178))))))))))) in (let TMP_180 \def (\lambda (u3:
900 T).(\lambda (_: T).(pr0 u1 u3))) in (let TMP_181 \def (\lambda (_:
901 T).(\lambda (t3: T).(pr0 t1 t3))) in (let TMP_182 \def (ex3_2 T T TMP_179
902 TMP_180 TMP_181) in (let TMP_183 \def (S O) in (let TMP_184 \def (Bind b) in
903 (let TMP_185 \def (Flat Appl) in (let TMP_186 \def (S O) in (let TMP_187 \def
904 (lift TMP_186 O v2) in (let TMP_188 \def (THead TMP_185 TMP_187 t2) in (let
905 TMP_189 \def (THead TMP_184 u2 TMP_188) in (let TMP_190 \def (lift TMP_183 O
906 TMP_189) in (let TMP_191 \def (pr0 t1 TMP_190) in (let TMP_192 \def (or
907 TMP_182 TMP_191) in (False_ind TMP_192
908 H9)))))))))))))))))))))))))))))))))))))) in (let TMP_213 \def (\lambda (u0:
909 T).(\lambda (u2: T).(\lambda (_: (pr0 u0 u2)).(\lambda (_: (((eq T u0 (THead
910 (Bind Void) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq
911 T u2 (THead (Bind Void) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1
912 u3))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O
913 u2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda
914 (_: (((eq T t0 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T (\lambda (u3:
915 T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u3 t3)))) (\lambda (u3:
916 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
917 t3)))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (w: T).(\lambda (_: (subst0 O
918 u2 t2 w)).(\lambda (H6: (eq T (THead (Bind Abbr) u0 t0) (THead (Bind Void) u1
919 t1))).(let TMP_194 \def (Bind Abbr) in (let TMP_195 \def (THead TMP_194 u0
920 t0) in (let TMP_196 \def (\lambda (ee: T).(match ee with [(TSort _)
921 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
922 (match k with [(Bind b) \Rightarrow (match b with [Abbr \Rightarrow True |
923 Abst \Rightarrow False | Void \Rightarrow False]) | (Flat _) \Rightarrow
924 False])])) in (let TMP_197 \def (Bind Void) in (let TMP_198 \def (THead
925 TMP_197 u1 t1) in (let H7 \def (eq_ind T TMP_195 TMP_196 I TMP_198 H6) in
926 (let TMP_203 \def (\lambda (u3: T).(\lambda (t3: T).(let TMP_199 \def (Bind
927 Abbr) in (let TMP_200 \def (THead TMP_199 u2 w) in (let TMP_201 \def (Bind
928 Void) in (let TMP_202 \def (THead TMP_201 u3 t3) in (eq T TMP_200
929 TMP_202))))))) in (let TMP_204 \def (\lambda (u3: T).(\lambda (_: T).(pr0 u1
930 u3))) in (let TMP_205 \def (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3))) in
931 (let TMP_206 \def (ex3_2 T T TMP_203 TMP_204 TMP_205) in (let TMP_207 \def (S
932 O) in (let TMP_208 \def (Bind Abbr) in (let TMP_209 \def (THead TMP_208 u2 w)
933 in (let TMP_210 \def (lift TMP_207 O TMP_209) in (let TMP_211 \def (pr0 t1
934 TMP_210) in (let TMP_212 \def (or TMP_206 TMP_211) in (False_ind TMP_212
935 H7)))))))))))))))))))))))))))) in (let TMP_293 \def (\lambda (b: B).(\lambda
936 (H1: (not (eq B b Abst))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H2:
937 (pr0 t0 t2)).(\lambda (H3: (((eq T t0 (THead (Bind Void) u1 t1)) \to (or
938 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u2
939 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
940 T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O t2)))))).(\lambda
941 (u: T).(\lambda (H4: (eq T (THead (Bind b) u (lift (S O) O t0)) (THead (Bind
942 Void) u1 t1))).(let TMP_214 \def (\lambda (e: T).(match e with [(TSort _)
943 \Rightarrow b | (TLRef _) \Rightarrow b | (THead k _ _) \Rightarrow (match k
944 with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow b])])) in (let TMP_215
945 \def (Bind b) in (let TMP_216 \def (S O) in (let TMP_217 \def (lift TMP_216 O
946 t0) in (let TMP_218 \def (THead TMP_215 u TMP_217) in (let TMP_219 \def (Bind
947 Void) in (let TMP_220 \def (THead TMP_219 u1 t1) in (let H5 \def (f_equal T B
948 TMP_214 TMP_218 TMP_220 H4) in (let TMP_221 \def (\lambda (e: T).(match e
949 with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t _)
950 \Rightarrow t])) in (let TMP_222 \def (Bind b) in (let TMP_223 \def (S O) in
951 (let TMP_224 \def (lift TMP_223 O t0) in (let TMP_225 \def (THead TMP_222 u
952 TMP_224) in (let TMP_226 \def (Bind Void) in (let TMP_227 \def (THead TMP_226
953 u1 t1) in (let H6 \def (f_equal T T TMP_221 TMP_225 TMP_227 H4) in (let
954 TMP_242 \def (\lambda (e: T).(match e with [(TSort _) \Rightarrow (let
955 TMP_241 \def (\lambda (x0: nat).(let TMP_240 \def (S O) in (plus x0
956 TMP_240))) in (lref_map TMP_241 O t0)) | (TLRef _) \Rightarrow (let TMP_234
957 \def (\lambda (x0: nat).(let TMP_233 \def (S O) in (plus x0 TMP_233))) in
958 (lref_map TMP_234 O t0)) | (THead _ _ t) \Rightarrow t])) in (let TMP_243
959 \def (Bind b) in (let TMP_244 \def (S O) in (let TMP_245 \def (lift TMP_244 O
960 t0) in (let TMP_246 \def (THead TMP_243 u TMP_245) in (let TMP_247 \def (Bind
961 Void) in (let TMP_248 \def (THead TMP_247 u1 t1) in (let H7 \def (f_equal T T
962 TMP_242 TMP_246 TMP_248 H4) in (let TMP_291 \def (\lambda (_: (eq T u
963 u1)).(\lambda (H9: (eq B b Void)).(let TMP_250 \def (\lambda (b0: B).(let
964 TMP_249 \def (eq B b0 Abst) in (not TMP_249))) in (let H10 \def (eq_ind B b
965 TMP_250 H1 Void H9) in (let TMP_260 \def (\lambda (t: T).((eq T t0 (THead
966 (Bind Void) u1 t)) \to (let TMP_253 \def (\lambda (u2: T).(\lambda (t3:
967 T).(let TMP_251 \def (Bind Void) in (let TMP_252 \def (THead TMP_251 u2 t3)
968 in (eq T t2 TMP_252))))) in (let TMP_254 \def (\lambda (u2: T).(\lambda (_:
969 T).(pr0 u1 u2))) in (let TMP_255 \def (\lambda (_: T).(\lambda (t3: T).(pr0 t
970 t3))) in (let TMP_256 \def (ex3_2 T T TMP_253 TMP_254 TMP_255) in (let
971 TMP_257 \def (S O) in (let TMP_258 \def (lift TMP_257 O t2) in (let TMP_259
972 \def (pr0 t TMP_258) in (or TMP_256 TMP_259)))))))))) in (let TMP_261 \def (S
973 O) in (let TMP_262 \def (lift TMP_261 O t0) in (let H11 \def (eq_ind_r T t1
974 TMP_260 H3 TMP_262 H7) in (let TMP_263 \def (S O) in (let TMP_264 \def (lift
975 TMP_263 O t0) in (let TMP_274 \def (\lambda (t: T).(let TMP_267 \def (\lambda
976 (u2: T).(\lambda (t3: T).(let TMP_265 \def (Bind Void) in (let TMP_266 \def
977 (THead TMP_265 u2 t3) in (eq T t2 TMP_266))))) in (let TMP_268 \def (\lambda
978 (u2: T).(\lambda (_: T).(pr0 u1 u2))) in (let TMP_269 \def (\lambda (_:
979 T).(\lambda (t3: T).(pr0 t t3))) in (let TMP_270 \def (ex3_2 T T TMP_267
980 TMP_268 TMP_269) in (let TMP_271 \def (S O) in (let TMP_272 \def (lift
981 TMP_271 O t2) in (let TMP_273 \def (pr0 t TMP_272) in (or TMP_270
982 TMP_273))))))))) in (let TMP_277 \def (\lambda (u2: T).(\lambda (t3: T).(let
983 TMP_275 \def (Bind Void) in (let TMP_276 \def (THead TMP_275 u2 t3) in (eq T
984 t2 TMP_276))))) in (let TMP_278 \def (\lambda (u2: T).(\lambda (_: T).(pr0 u1
985 u2))) in (let TMP_281 \def (\lambda (_: T).(\lambda (t3: T).(let TMP_279 \def
986 (S O) in (let TMP_280 \def (lift TMP_279 O t0) in (pr0 TMP_280 t3))))) in
987 (let TMP_282 \def (ex3_2 T T TMP_277 TMP_278 TMP_281) in (let TMP_283 \def (S
988 O) in (let TMP_284 \def (lift TMP_283 O t0) in (let TMP_285 \def (S O) in
989 (let TMP_286 \def (lift TMP_285 O t2) in (let TMP_287 \def (pr0 TMP_284
990 TMP_286) in (let TMP_288 \def (S O) in (let TMP_289 \def (pr0_lift t0 t2 H2
991 TMP_288 O) in (let TMP_290 \def (or_intror TMP_282 TMP_287 TMP_289) in
992 (eq_ind T TMP_264 TMP_274 TMP_290 t1 H7)))))))))))))))))))))))) in (let
993 TMP_292 \def (TMP_291 H6) in (TMP_292 H5)))))))))))))))))))))))))))))))))))
994 in (let TMP_309 \def (\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0
995 t2)).(\lambda (_: (((eq T t0 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T
996 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u2 t3))))
997 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
998 T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (u: T).(\lambda
999 (H3: (eq T (THead (Flat Cast) u t0) (THead (Bind Void) u1 t1))).(let TMP_294
1000 \def (Flat Cast) in (let TMP_295 \def (THead TMP_294 u t0) in (let TMP_296
1001 \def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
1002 \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _)
1003 \Rightarrow False | (Flat _) \Rightarrow True])])) in (let TMP_297 \def (Bind
1004 Void) in (let TMP_298 \def (THead TMP_297 u1 t1) in (let H4 \def (eq_ind T
1005 TMP_295 TMP_296 I TMP_298 H3) in (let TMP_301 \def (\lambda (u2: T).(\lambda
1006 (t3: T).(let TMP_299 \def (Bind Void) in (let TMP_300 \def (THead TMP_299 u2
1007 t3) in (eq T t2 TMP_300))))) in (let TMP_302 \def (\lambda (u2: T).(\lambda
1008 (_: T).(pr0 u1 u2))) in (let TMP_303 \def (\lambda (_: T).(\lambda (t3:
1009 T).(pr0 t1 t3))) in (let TMP_304 \def (ex3_2 T T TMP_301 TMP_302 TMP_303) in
1010 (let TMP_305 \def (S O) in (let TMP_306 \def (lift TMP_305 O t2) in (let
1011 TMP_307 \def (pr0 t1 TMP_306) in (let TMP_308 \def (or TMP_304 TMP_307) in
1012 (False_ind TMP_308 H4))))))))))))))))))))) in (pr0_ind TMP_23 TMP_66 TMP_141
1013 TMP_163 TMP_193 TMP_213 TMP_293 TMP_309 y x H0))))))))))) in (insert_eq T
1014 TMP_2 TMP_3 TMP_13 TMP_310 H))))))))).
projects / helm.git / blob