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/ty3/arity.ma".
19 include "basic_1/pc3/nf2.ma".
21 include "basic_1/nf2/arity.ma".
23 definition ty3_nf2_inv_abst_premise:
24 C \to (T \to (T \to Prop))
26 \lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\forall (d: C).(\forall (wi:
27 T).(\forall (i: nat).((getl i c (CHead d (Bind Abst) wi)) \to (\forall (vs:
28 TList).((pc3 c (THeads (Flat Appl) vs (lift (S i) O wi)) (THead (Bind Abst) w
29 u)) \to False)))))))).
31 theorem ty3_nf2_inv_abst_premise_csort:
32 \forall (w: T).(\forall (u: T).(\forall (m: nat).(ty3_nf2_inv_abst_premise
35 \lambda (w: T).(\lambda (u: T).(\lambda (m: nat).(\lambda (d: C).(\lambda
36 (wi: T).(\lambda (i: nat).(\lambda (H: (getl i (CSort m) (CHead d (Bind Abst)
37 wi))).(\lambda (vs: TList).(\lambda (_: (pc3 (CSort m) (THeads (Flat Appl) vs
38 (lift (S i) O wi)) (THead (Bind Abst) w u))).(let TMP_1 \def (Bind Abst) in
39 (let TMP_2 \def (CHead d TMP_1 wi) in (getl_gen_sort m i TMP_2 H
42 theorem ty3_nf2_inv_all:
43 \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (u: T).((ty3 g c t
44 u) \to ((nf2 c t) \to (or3 (ex3_2 T T (\lambda (w: T).(\lambda (u0: T).(eq T
45 t (THead (Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 c w)))
46 (\lambda (w: T).(\lambda (u0: T).(nf2 (CHead c (Bind Abst) w) u0)))) (ex nat
47 (\lambda (n: nat).(eq T t (TSort n)))) (ex3_2 TList nat (\lambda (ws:
48 TList).(\lambda (i: nat).(eq T t (THeads (Flat Appl) ws (TLRef i)))))
49 (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_:
50 TList).(\lambda (i: nat).(nf2 c (TLRef i)))))))))))
52 \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (u: T).(\lambda (H:
53 (ty3 g c t u)).(\lambda (H0: (nf2 c t)).(let H_x \def (ty3_arity g c t u H)
54 in (let H1 \def H_x in (let TMP_1 \def (\lambda (a1: A).(arity g c t a1)) in
55 (let TMP_3 \def (\lambda (a1: A).(let TMP_2 \def (asucc g a1) in (arity g c u
56 TMP_2))) in (let TMP_6 \def (\lambda (w: T).(\lambda (u0: T).(let TMP_4 \def
57 (Bind Abst) in (let TMP_5 \def (THead TMP_4 w u0) in (eq T t TMP_5))))) in
58 (let TMP_7 \def (\lambda (w: T).(\lambda (_: T).(nf2 c w))) in (let TMP_10
59 \def (\lambda (w: T).(\lambda (u0: T).(let TMP_8 \def (Bind Abst) in (let
60 TMP_9 \def (CHead c TMP_8 w) in (nf2 TMP_9 u0))))) in (let TMP_11 \def (ex3_2
61 T T TMP_6 TMP_7 TMP_10) in (let TMP_13 \def (\lambda (n: nat).(let TMP_12
62 \def (TSort n) in (eq T t TMP_12))) in (let TMP_14 \def (ex nat TMP_13) in
63 (let TMP_18 \def (\lambda (ws: TList).(\lambda (i: nat).(let TMP_15 \def
64 (Flat Appl) in (let TMP_16 \def (TLRef i) in (let TMP_17 \def (THeads TMP_15
65 ws TMP_16) in (eq T t TMP_17)))))) in (let TMP_19 \def (\lambda (ws:
66 TList).(\lambda (_: nat).(nfs2 c ws))) in (let TMP_21 \def (\lambda (_:
67 TList).(\lambda (i: nat).(let TMP_20 \def (TLRef i) in (nf2 c TMP_20)))) in
68 (let TMP_22 \def (ex3_2 TList nat TMP_18 TMP_19 TMP_21) in (let TMP_23 \def
69 (or3 TMP_11 TMP_14 TMP_22) in (let TMP_24 \def (\lambda (x: A).(\lambda (H2:
70 (arity g c t x)).(\lambda (_: (arity g c u (asucc g x))).(arity_nf2_inv_all g
71 c t x H2 H0)))) in (ex2_ind A TMP_1 TMP_3 TMP_23 TMP_24
72 H1)))))))))))))))))))))).
74 theorem ty3_nf2_inv_sort:
75 \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (m: nat).((ty3 g c t
76 (TSort m)) \to ((nf2 c t) \to (or (ex2 nat (\lambda (n: nat).(eq T t (TSort
77 n))) (\lambda (n: nat).(eq nat m (next g n)))) (ex3_2 TList nat (\lambda (ws:
78 TList).(\lambda (i: nat).(eq T t (THeads (Flat Appl) ws (TLRef i)))))
79 (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_:
80 TList).(\lambda (i: nat).(nf2 c (TLRef i)))))))))))
82 \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (m: nat).(\lambda
83 (H: (ty3 g c t (TSort m))).(\lambda (H0: (nf2 c t)).(let TMP_1 \def (TSort m)
84 in (let H_x \def (ty3_nf2_inv_all g c t TMP_1 H H0) in (let H1 \def H_x in
85 (let TMP_4 \def (\lambda (w: T).(\lambda (u: T).(let TMP_2 \def (Bind Abst)
86 in (let TMP_3 \def (THead TMP_2 w u) in (eq T t TMP_3))))) in (let TMP_5 \def
87 (\lambda (w: T).(\lambda (_: T).(nf2 c w))) in (let TMP_8 \def (\lambda (w:
88 T).(\lambda (u: T).(let TMP_6 \def (Bind Abst) in (let TMP_7 \def (CHead c
89 TMP_6 w) in (nf2 TMP_7 u))))) in (let TMP_9 \def (ex3_2 T T TMP_4 TMP_5
90 TMP_8) in (let TMP_11 \def (\lambda (n: nat).(let TMP_10 \def (TSort n) in
91 (eq T t TMP_10))) in (let TMP_12 \def (ex nat TMP_11) in (let TMP_16 \def
92 (\lambda (ws: TList).(\lambda (i: nat).(let TMP_13 \def (Flat Appl) in (let
93 TMP_14 \def (TLRef i) in (let TMP_15 \def (THeads TMP_13 ws TMP_14) in (eq T
94 t TMP_15)))))) in (let TMP_17 \def (\lambda (ws: TList).(\lambda (_:
95 nat).(nfs2 c ws))) in (let TMP_19 \def (\lambda (_: TList).(\lambda (i:
96 nat).(let TMP_18 \def (TLRef i) in (nf2 c TMP_18)))) in (let TMP_20 \def
97 (ex3_2 TList nat TMP_16 TMP_17 TMP_19) in (let TMP_22 \def (\lambda (n:
98 nat).(let TMP_21 \def (TSort n) in (eq T t TMP_21))) in (let TMP_24 \def
99 (\lambda (n: nat).(let TMP_23 \def (next g n) in (eq nat m TMP_23))) in (let
100 TMP_25 \def (ex2 nat TMP_22 TMP_24) in (let TMP_29 \def (\lambda (ws:
101 TList).(\lambda (i: nat).(let TMP_26 \def (Flat Appl) in (let TMP_27 \def
102 (TLRef i) in (let TMP_28 \def (THeads TMP_26 ws TMP_27) in (eq T t
103 TMP_28)))))) in (let TMP_30 \def (\lambda (ws: TList).(\lambda (_: nat).(nfs2
104 c ws))) in (let TMP_32 \def (\lambda (_: TList).(\lambda (i: nat).(let TMP_31
105 \def (TLRef i) in (nf2 c TMP_31)))) in (let TMP_33 \def (ex3_2 TList nat
106 TMP_29 TMP_30 TMP_32) in (let TMP_34 \def (or TMP_25 TMP_33) in (let TMP_129
107 \def (\lambda (H2: (ex3_2 T T (\lambda (w: T).(\lambda (u: T).(eq T t (THead
108 (Bind Abst) w u)))) (\lambda (w: T).(\lambda (_: T).(nf2 c w))) (\lambda (w:
109 T).(\lambda (u: T).(nf2 (CHead c (Bind Abst) w) u))))).(let TMP_37 \def
110 (\lambda (w: T).(\lambda (u: T).(let TMP_35 \def (Bind Abst) in (let TMP_36
111 \def (THead TMP_35 w u) in (eq T t TMP_36))))) in (let TMP_38 \def (\lambda
112 (w: T).(\lambda (_: T).(nf2 c w))) in (let TMP_41 \def (\lambda (w:
113 T).(\lambda (u: T).(let TMP_39 \def (Bind Abst) in (let TMP_40 \def (CHead c
114 TMP_39 w) in (nf2 TMP_40 u))))) in (let TMP_43 \def (\lambda (n: nat).(let
115 TMP_42 \def (TSort n) in (eq T t TMP_42))) in (let TMP_45 \def (\lambda (n:
116 nat).(let TMP_44 \def (next g n) in (eq nat m TMP_44))) in (let TMP_46 \def
117 (ex2 nat TMP_43 TMP_45) in (let TMP_50 \def (\lambda (ws: TList).(\lambda (i:
118 nat).(let TMP_47 \def (Flat Appl) in (let TMP_48 \def (TLRef i) in (let
119 TMP_49 \def (THeads TMP_47 ws TMP_48) in (eq T t TMP_49)))))) in (let TMP_51
120 \def (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) in (let TMP_53 \def
121 (\lambda (_: TList).(\lambda (i: nat).(let TMP_52 \def (TLRef i) in (nf2 c
122 TMP_52)))) in (let TMP_54 \def (ex3_2 TList nat TMP_50 TMP_51 TMP_53) in (let
123 TMP_55 \def (or TMP_46 TMP_54) in (let TMP_128 \def (\lambda (x0: T).(\lambda
124 (x1: T).(\lambda (H3: (eq T t (THead (Bind Abst) x0 x1))).(\lambda (_: (nf2 c
125 x0)).(\lambda (_: (nf2 (CHead c (Bind Abst) x0) x1)).(let TMP_57 \def
126 (\lambda (t0: T).(let TMP_56 \def (TSort m) in (ty3 g c t0 TMP_56))) in (let
127 TMP_58 \def (Bind Abst) in (let TMP_59 \def (THead TMP_58 x0 x1) in (let H6
128 \def (eq_ind T t TMP_57 H TMP_59 H3) in (let TMP_60 \def (Bind Abst) in (let
129 TMP_61 \def (THead TMP_60 x0 x1) in (let TMP_75 \def (\lambda (t0: T).(let
130 TMP_63 \def (\lambda (n: nat).(let TMP_62 \def (TSort n) in (eq T t0
131 TMP_62))) in (let TMP_65 \def (\lambda (n: nat).(let TMP_64 \def (next g n)
132 in (eq nat m TMP_64))) in (let TMP_66 \def (ex2 nat TMP_63 TMP_65) in (let
133 TMP_70 \def (\lambda (ws: TList).(\lambda (i: nat).(let TMP_67 \def (Flat
134 Appl) in (let TMP_68 \def (TLRef i) in (let TMP_69 \def (THeads TMP_67 ws
135 TMP_68) in (eq T t0 TMP_69)))))) in (let TMP_71 \def (\lambda (ws:
136 TList).(\lambda (_: nat).(nfs2 c ws))) in (let TMP_73 \def (\lambda (_:
137 TList).(\lambda (i: nat).(let TMP_72 \def (TLRef i) in (nf2 c TMP_72)))) in
138 (let TMP_74 \def (ex3_2 TList nat TMP_70 TMP_71 TMP_73) in (or TMP_66
139 TMP_74))))))))) in (let TMP_79 \def (\lambda (t2: T).(\lambda (_: T).(let
140 TMP_76 \def (Bind Abst) in (let TMP_77 \def (THead TMP_76 x0 t2) in (let
141 TMP_78 \def (TSort m) in (pc3 c TMP_77 TMP_78)))))) in (let TMP_80 \def
142 (\lambda (_: T).(\lambda (t0: T).(ty3 g c x0 t0))) in (let TMP_83 \def
143 (\lambda (t2: T).(\lambda (_: T).(let TMP_81 \def (Bind Abst) in (let TMP_82
144 \def (CHead c TMP_81 x0) in (ty3 g TMP_82 x1 t2))))) in (let TMP_87 \def
145 (\lambda (n: nat).(let TMP_84 \def (Bind Abst) in (let TMP_85 \def (THead
146 TMP_84 x0 x1) in (let TMP_86 \def (TSort n) in (eq T TMP_85 TMP_86))))) in
147 (let TMP_89 \def (\lambda (n: nat).(let TMP_88 \def (next g n) in (eq nat m
148 TMP_88))) in (let TMP_90 \def (ex2 nat TMP_87 TMP_89) in (let TMP_96 \def
149 (\lambda (ws: TList).(\lambda (i: nat).(let TMP_91 \def (Bind Abst) in (let
150 TMP_92 \def (THead TMP_91 x0 x1) in (let TMP_93 \def (Flat Appl) in (let
151 TMP_94 \def (TLRef i) in (let TMP_95 \def (THeads TMP_93 ws TMP_94) in (eq T
152 TMP_92 TMP_95)))))))) in (let TMP_97 \def (\lambda (ws: TList).(\lambda (_:
153 nat).(nfs2 c ws))) in (let TMP_99 \def (\lambda (_: TList).(\lambda (i:
154 nat).(let TMP_98 \def (TLRef i) in (nf2 c TMP_98)))) in (let TMP_100 \def
155 (ex3_2 TList nat TMP_96 TMP_97 TMP_99) in (let TMP_101 \def (or TMP_90
156 TMP_100) in (let TMP_124 \def (\lambda (x2: T).(\lambda (x3: T).(\lambda (H7:
157 (pc3 c (THead (Bind Abst) x0 x2) (TSort m))).(\lambda (_: (ty3 g c x0
158 x3)).(\lambda (_: (ty3 g (CHead c (Bind Abst) x0) x1 x2)).(let TMP_102 \def
159 (TSort m) in (let TMP_103 \def (Bind Abst) in (let TMP_104 \def (THead
160 TMP_103 x0 x2) in (let TMP_105 \def (pc3_s c TMP_102 TMP_104 H7) in (let
161 TMP_109 \def (\lambda (n: nat).(let TMP_106 \def (Bind Abst) in (let TMP_107
162 \def (THead TMP_106 x0 x1) in (let TMP_108 \def (TSort n) in (eq T TMP_107
163 TMP_108))))) in (let TMP_111 \def (\lambda (n: nat).(let TMP_110 \def (next g
164 n) in (eq nat m TMP_110))) in (let TMP_112 \def (ex2 nat TMP_109 TMP_111) in
165 (let TMP_118 \def (\lambda (ws: TList).(\lambda (i: nat).(let TMP_113 \def
166 (Bind Abst) in (let TMP_114 \def (THead TMP_113 x0 x1) in (let TMP_115 \def
167 (Flat Appl) in (let TMP_116 \def (TLRef i) in (let TMP_117 \def (THeads
168 TMP_115 ws TMP_116) in (eq T TMP_114 TMP_117)))))))) in (let TMP_119 \def
169 (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) in (let TMP_121 \def
170 (\lambda (_: TList).(\lambda (i: nat).(let TMP_120 \def (TLRef i) in (nf2 c
171 TMP_120)))) in (let TMP_122 \def (ex3_2 TList nat TMP_118 TMP_119 TMP_121) in
172 (let TMP_123 \def (or TMP_112 TMP_122) in (pc3_gen_sort_abst c x0 x2 m
173 TMP_105 TMP_123)))))))))))))))))) in (let TMP_125 \def (TSort m) in (let
174 TMP_126 \def (ty3_gen_bind g Abst c x0 x1 TMP_125 H6) in (let TMP_127 \def
175 (ex3_2_ind T T TMP_79 TMP_80 TMP_83 TMP_101 TMP_124 TMP_126) in (eq_ind_r T
176 TMP_61 TMP_75 TMP_127 t H3)))))))))))))))))))))))))))) in (ex3_2_ind T T
177 TMP_37 TMP_38 TMP_41 TMP_55 TMP_128 H2)))))))))))))) in (let TMP_215 \def
178 (\lambda (H2: (ex nat (\lambda (n: nat).(eq T t (TSort n))))).(let TMP_131
179 \def (\lambda (n: nat).(let TMP_130 \def (TSort n) in (eq T t TMP_130))) in
180 (let TMP_133 \def (\lambda (n: nat).(let TMP_132 \def (TSort n) in (eq T t
181 TMP_132))) in (let TMP_135 \def (\lambda (n: nat).(let TMP_134 \def (next g
182 n) in (eq nat m TMP_134))) in (let TMP_136 \def (ex2 nat TMP_133 TMP_135) in
183 (let TMP_140 \def (\lambda (ws: TList).(\lambda (i: nat).(let TMP_137 \def
184 (Flat Appl) in (let TMP_138 \def (TLRef i) in (let TMP_139 \def (THeads
185 TMP_137 ws TMP_138) in (eq T t TMP_139)))))) in (let TMP_141 \def (\lambda
186 (ws: TList).(\lambda (_: nat).(nfs2 c ws))) in (let TMP_143 \def (\lambda (_:
187 TList).(\lambda (i: nat).(let TMP_142 \def (TLRef i) in (nf2 c TMP_142)))) in
188 (let TMP_144 \def (ex3_2 TList nat TMP_140 TMP_141 TMP_143) in (let TMP_145
189 \def (or TMP_136 TMP_144) in (let TMP_214 \def (\lambda (x: nat).(\lambda
190 (H3: (eq T t (TSort x))).(let TMP_147 \def (\lambda (t0: T).(let TMP_146 \def
191 (TSort m) in (ty3 g c t0 TMP_146))) in (let TMP_148 \def (TSort x) in (let H4
192 \def (eq_ind T t TMP_147 H TMP_148 H3) in (let TMP_149 \def (TSort x) in (let
193 TMP_163 \def (\lambda (t0: T).(let TMP_151 \def (\lambda (n: nat).(let
194 TMP_150 \def (TSort n) in (eq T t0 TMP_150))) in (let TMP_153 \def (\lambda
195 (n: nat).(let TMP_152 \def (next g n) in (eq nat m TMP_152))) in (let TMP_154
196 \def (ex2 nat TMP_151 TMP_153) in (let TMP_158 \def (\lambda (ws:
197 TList).(\lambda (i: nat).(let TMP_155 \def (Flat Appl) in (let TMP_156 \def
198 (TLRef i) in (let TMP_157 \def (THeads TMP_155 ws TMP_156) in (eq T t0
199 TMP_157)))))) in (let TMP_159 \def (\lambda (ws: TList).(\lambda (_:
200 nat).(nfs2 c ws))) in (let TMP_161 \def (\lambda (_: TList).(\lambda (i:
201 nat).(let TMP_160 \def (TLRef i) in (nf2 c TMP_160)))) in (let TMP_162 \def
202 (ex3_2 TList nat TMP_158 TMP_159 TMP_161) in (or TMP_154 TMP_162))))))))) in
203 (let TMP_164 \def (next g x) in (let TMP_180 \def (\lambda (n: nat).(let
204 TMP_167 \def (\lambda (n0: nat).(let TMP_165 \def (TSort x) in (let TMP_166
205 \def (TSort n0) in (eq T TMP_165 TMP_166)))) in (let TMP_169 \def (\lambda
206 (n0: nat).(let TMP_168 \def (next g n0) in (eq nat n TMP_168))) in (let
207 TMP_170 \def (ex2 nat TMP_167 TMP_169) in (let TMP_175 \def (\lambda (ws:
208 TList).(\lambda (i: nat).(let TMP_171 \def (TSort x) in (let TMP_172 \def
209 (Flat Appl) in (let TMP_173 \def (TLRef i) in (let TMP_174 \def (THeads
210 TMP_172 ws TMP_173) in (eq T TMP_171 TMP_174))))))) in (let TMP_176 \def
211 (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) in (let TMP_178 \def
212 (\lambda (_: TList).(\lambda (i: nat).(let TMP_177 \def (TLRef i) in (nf2 c
213 TMP_177)))) in (let TMP_179 \def (ex3_2 TList nat TMP_175 TMP_176 TMP_178) in
214 (or TMP_170 TMP_179))))))))) in (let TMP_183 \def (\lambda (n: nat).(let
215 TMP_181 \def (TSort x) in (let TMP_182 \def (TSort n) in (eq T TMP_181
216 TMP_182)))) in (let TMP_186 \def (\lambda (n: nat).(let TMP_184 \def (next g
217 x) in (let TMP_185 \def (next g n) in (eq nat TMP_184 TMP_185)))) in (let
218 TMP_187 \def (ex2 nat TMP_183 TMP_186) in (let TMP_192 \def (\lambda (ws:
219 TList).(\lambda (i: nat).(let TMP_188 \def (TSort x) in (let TMP_189 \def
220 (Flat Appl) in (let TMP_190 \def (TLRef i) in (let TMP_191 \def (THeads
221 TMP_189 ws TMP_190) in (eq T TMP_188 TMP_191))))))) in (let TMP_193 \def
222 (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) in (let TMP_195 \def
223 (\lambda (_: TList).(\lambda (i: nat).(let TMP_194 \def (TLRef i) in (nf2 c
224 TMP_194)))) in (let TMP_196 \def (ex3_2 TList nat TMP_192 TMP_193 TMP_195) in
225 (let TMP_199 \def (\lambda (n: nat).(let TMP_197 \def (TSort x) in (let
226 TMP_198 \def (TSort n) in (eq T TMP_197 TMP_198)))) in (let TMP_202 \def
227 (\lambda (n: nat).(let TMP_200 \def (next g x) in (let TMP_201 \def (next g
228 n) in (eq nat TMP_200 TMP_201)))) in (let TMP_203 \def (TSort x) in (let
229 TMP_204 \def (refl_equal T TMP_203) in (let TMP_205 \def (next g x) in (let
230 TMP_206 \def (refl_equal nat TMP_205) in (let TMP_207 \def (ex_intro2 nat
231 TMP_199 TMP_202 x TMP_204 TMP_206) in (let TMP_208 \def (or_introl TMP_187
232 TMP_196 TMP_207) in (let TMP_209 \def (next g x) in (let TMP_210 \def (TSort
233 m) in (let TMP_211 \def (ty3_gen_sort g c TMP_210 x H4) in (let TMP_212 \def
234 (pc3_gen_sort c TMP_209 m TMP_211) in (let TMP_213 \def (eq_ind nat TMP_164
235 TMP_180 TMP_208 m TMP_212) in (eq_ind_r T TMP_149 TMP_163 TMP_213 t
236 H3)))))))))))))))))))))))))))))) in (ex_ind nat TMP_131 TMP_145 TMP_214
237 H2)))))))))))) in (let TMP_295 \def (\lambda (H2: (ex3_2 TList nat (\lambda
238 (ws: TList).(\lambda (i: nat).(eq T t (THeads (Flat Appl) ws (TLRef i)))))
239 (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_:
240 TList).(\lambda (i: nat).(nf2 c (TLRef i)))))).(let TMP_219 \def (\lambda
241 (ws: TList).(\lambda (i: nat).(let TMP_216 \def (Flat Appl) in (let TMP_217
242 \def (TLRef i) in (let TMP_218 \def (THeads TMP_216 ws TMP_217) in (eq T t
243 TMP_218)))))) in (let TMP_220 \def (\lambda (ws: TList).(\lambda (_:
244 nat).(nfs2 c ws))) in (let TMP_222 \def (\lambda (_: TList).(\lambda (i:
245 nat).(let TMP_221 \def (TLRef i) in (nf2 c TMP_221)))) in (let TMP_224 \def
246 (\lambda (n: nat).(let TMP_223 \def (TSort n) in (eq T t TMP_223))) in (let
247 TMP_226 \def (\lambda (n: nat).(let TMP_225 \def (next g n) in (eq nat m
248 TMP_225))) in (let TMP_227 \def (ex2 nat TMP_224 TMP_226) in (let TMP_231
249 \def (\lambda (ws: TList).(\lambda (i: nat).(let TMP_228 \def (Flat Appl) in
250 (let TMP_229 \def (TLRef i) in (let TMP_230 \def (THeads TMP_228 ws TMP_229)
251 in (eq T t TMP_230)))))) in (let TMP_232 \def (\lambda (ws: TList).(\lambda
252 (_: nat).(nfs2 c ws))) in (let TMP_234 \def (\lambda (_: TList).(\lambda (i:
253 nat).(let TMP_233 \def (TLRef i) in (nf2 c TMP_233)))) in (let TMP_235 \def
254 (ex3_2 TList nat TMP_231 TMP_232 TMP_234) in (let TMP_236 \def (or TMP_227
255 TMP_235) in (let TMP_294 \def (\lambda (x0: TList).(\lambda (x1:
256 nat).(\lambda (H3: (eq T t (THeads (Flat Appl) x0 (TLRef x1)))).(\lambda (H4:
257 (nfs2 c x0)).(\lambda (H5: (nf2 c (TLRef x1))).(let TMP_238 \def (\lambda
258 (t0: T).(let TMP_237 \def (TSort m) in (ty3 g c t0 TMP_237))) in (let TMP_239
259 \def (Flat Appl) in (let TMP_240 \def (TLRef x1) in (let TMP_241 \def (THeads
260 TMP_239 x0 TMP_240) in (let H6 \def (eq_ind T t TMP_238 H TMP_241 H3) in (let
261 TMP_242 \def (Flat Appl) in (let TMP_243 \def (TLRef x1) in (let TMP_244 \def
262 (THeads TMP_242 x0 TMP_243) in (let TMP_258 \def (\lambda (t0: T).(let
263 TMP_246 \def (\lambda (n: nat).(let TMP_245 \def (TSort n) in (eq T t0
264 TMP_245))) in (let TMP_248 \def (\lambda (n: nat).(let TMP_247 \def (next g
265 n) in (eq nat m TMP_247))) in (let TMP_249 \def (ex2 nat TMP_246 TMP_248) in
266 (let TMP_253 \def (\lambda (ws: TList).(\lambda (i: nat).(let TMP_250 \def
267 (Flat Appl) in (let TMP_251 \def (TLRef i) in (let TMP_252 \def (THeads
268 TMP_250 ws TMP_251) in (eq T t0 TMP_252)))))) in (let TMP_254 \def (\lambda
269 (ws: TList).(\lambda (_: nat).(nfs2 c ws))) in (let TMP_256 \def (\lambda (_:
270 TList).(\lambda (i: nat).(let TMP_255 \def (TLRef i) in (nf2 c TMP_255)))) in
271 (let TMP_257 \def (ex3_2 TList nat TMP_253 TMP_254 TMP_256) in (or TMP_249
272 TMP_257))))))))) in (let TMP_263 \def (\lambda (n: nat).(let TMP_259 \def
273 (Flat Appl) in (let TMP_260 \def (TLRef x1) in (let TMP_261 \def (THeads
274 TMP_259 x0 TMP_260) in (let TMP_262 \def (TSort n) in (eq T TMP_261
275 TMP_262)))))) in (let TMP_265 \def (\lambda (n: nat).(let TMP_264 \def (next
276 g n) in (eq nat m TMP_264))) in (let TMP_266 \def (ex2 nat TMP_263 TMP_265)
277 in (let TMP_273 \def (\lambda (ws: TList).(\lambda (i: nat).(let TMP_267 \def
278 (Flat Appl) in (let TMP_268 \def (TLRef x1) in (let TMP_269 \def (THeads
279 TMP_267 x0 TMP_268) in (let TMP_270 \def (Flat Appl) in (let TMP_271 \def
280 (TLRef i) in (let TMP_272 \def (THeads TMP_270 ws TMP_271) in (eq T TMP_269
281 TMP_272))))))))) in (let TMP_274 \def (\lambda (ws: TList).(\lambda (_:
282 nat).(nfs2 c ws))) in (let TMP_276 \def (\lambda (_: TList).(\lambda (i:
283 nat).(let TMP_275 \def (TLRef i) in (nf2 c TMP_275)))) in (let TMP_277 \def
284 (ex3_2 TList nat TMP_273 TMP_274 TMP_276) in (let TMP_284 \def (\lambda (ws:
285 TList).(\lambda (i: nat).(let TMP_278 \def (Flat Appl) in (let TMP_279 \def
286 (TLRef x1) in (let TMP_280 \def (THeads TMP_278 x0 TMP_279) in (let TMP_281
287 \def (Flat Appl) in (let TMP_282 \def (TLRef i) in (let TMP_283 \def (THeads
288 TMP_281 ws TMP_282) in (eq T TMP_280 TMP_283))))))))) in (let TMP_285 \def
289 (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) in (let TMP_287 \def
290 (\lambda (_: TList).(\lambda (i: nat).(let TMP_286 \def (TLRef i) in (nf2 c
291 TMP_286)))) in (let TMP_288 \def (Flat Appl) in (let TMP_289 \def (TLRef x1)
292 in (let TMP_290 \def (THeads TMP_288 x0 TMP_289) in (let TMP_291 \def
293 (refl_equal T TMP_290) in (let TMP_292 \def (ex3_2_intro TList nat TMP_284
294 TMP_285 TMP_287 x0 x1 TMP_291 H4 H5) in (let TMP_293 \def (or_intror TMP_266
295 TMP_277 TMP_292) in (eq_ind_r T TMP_244 TMP_258 TMP_293 t
296 H3))))))))))))))))))))))))))))))) in (ex3_2_ind TList nat TMP_219 TMP_220
297 TMP_222 TMP_236 TMP_294 H2)))))))))))))) in (or3_ind TMP_9 TMP_12 TMP_20
298 TMP_34 TMP_129 TMP_215 TMP_295 H1)))))))))))))))))))))))))))))).
300 theorem ty3_nf2_gen__ty3_nf2_inv_abst_aux:
301 \forall (c: C).(\forall (w1: T).(\forall (u1: T).((ty3_nf2_inv_abst_premise
302 c w1 u1) \to (\forall (t: T).(\forall (w2: T).(\forall (u2: T).((pc3 c (THead
303 (Flat Appl) t (THead (Bind Abst) w2 u2)) (THead (Bind Abst) w1 u1)) \to
304 (ty3_nf2_inv_abst_premise c w2 u2))))))))
306 \lambda (c: C).(\lambda (w1: T).(\lambda (u1: T).(\lambda (H: ((\forall (d:
307 C).(\forall (wi: T).(\forall (i: nat).((getl i c (CHead d (Bind Abst) wi))
308 \to (\forall (vs: TList).((pc3 c (THeads (Flat Appl) vs (lift (S i) O wi))
309 (THead (Bind Abst) w1 u1)) \to False)))))))).(\lambda (t: T).(\lambda (w2:
310 T).(\lambda (u2: T).(\lambda (H0: (pc3 c (THead (Flat Appl) t (THead (Bind
311 Abst) w2 u2)) (THead (Bind Abst) w1 u1))).(\lambda (d: C).(\lambda (wi:
312 T).(\lambda (i: nat).(\lambda (H1: (getl i c (CHead d (Bind Abst)
313 wi))).(\lambda (vs: TList).(\lambda (H2: (pc3 c (THeads (Flat Appl) vs (lift
314 (S i) O wi)) (THead (Bind Abst) w2 u2))).(let TMP_1 \def (TCons t vs) in (let
315 TMP_2 \def (Flat Appl) in (let TMP_3 \def (Bind Abst) in (let TMP_4 \def
316 (THead TMP_3 w2 u2) in (let TMP_5 \def (THead TMP_2 t TMP_4) in (let TMP_6
317 \def (Flat Appl) in (let TMP_7 \def (Flat Appl) in (let TMP_8 \def (S i) in
318 (let TMP_9 \def (lift TMP_8 O wi) in (let TMP_10 \def (THeads TMP_7 vs TMP_9)
319 in (let TMP_11 \def (THead TMP_6 t TMP_10) in (let TMP_12 \def (Flat Appl) in
320 (let TMP_13 \def (S i) in (let TMP_14 \def (lift TMP_13 O wi) in (let TMP_15
321 \def (THeads TMP_12 vs TMP_14) in (let TMP_16 \def (Bind Abst) in (let TMP_17
322 \def (THead TMP_16 w2 u2) in (let TMP_18 \def (pc3_thin_dx c TMP_15 TMP_17 H2
323 t Appl) in (let TMP_19 \def (Bind Abst) in (let TMP_20 \def (THead TMP_19 w1
324 u1) in (let TMP_21 \def (pc3_t TMP_5 c TMP_11 TMP_18 TMP_20 H0) in (H d wi i
325 H1 TMP_1 TMP_21))))))))))))))))))))))))))))))))))).
327 theorem ty3_nf2_inv_abst:
328 \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (w: T).(\forall (u:
329 T).((ty3 g c t (THead (Bind Abst) w u)) \to ((nf2 c t) \to ((nf2 c w) \to
330 ((ty3_nf2_inv_abst_premise c w u) \to (ex4_2 T T (\lambda (v: T).(\lambda (_:
331 T).(eq T t (THead (Bind Abst) w v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g
332 c w w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) w) v
333 u))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w)
336 \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (w: T).(\lambda (u:
337 T).(\lambda (H: (ty3 g c t (THead (Bind Abst) w u))).(\lambda (H0: (nf2 c
338 t)).(\lambda (H1: (nf2 c w)).(\lambda (H2: (ty3_nf2_inv_abst_premise c w
339 u)).(let TMP_1 \def (Bind Abst) in (let TMP_2 \def (THead TMP_1 w u) in (let
340 H_x \def (ty3_nf2_inv_all g c t TMP_2 H H0) in (let H3 \def H_x in (let TMP_5
341 \def (\lambda (w0: T).(\lambda (u0: T).(let TMP_3 \def (Bind Abst) in (let
342 TMP_4 \def (THead TMP_3 w0 u0) in (eq T t TMP_4))))) in (let TMP_6 \def
343 (\lambda (w0: T).(\lambda (_: T).(nf2 c w0))) in (let TMP_9 \def (\lambda
344 (w0: T).(\lambda (u0: T).(let TMP_7 \def (Bind Abst) in (let TMP_8 \def
345 (CHead c TMP_7 w0) in (nf2 TMP_8 u0))))) in (let TMP_10 \def (ex3_2 T T TMP_5
346 TMP_6 TMP_9) in (let TMP_12 \def (\lambda (n: nat).(let TMP_11 \def (TSort n)
347 in (eq T t TMP_11))) in (let TMP_13 \def (ex nat TMP_12) in (let TMP_17 \def
348 (\lambda (ws: TList).(\lambda (i: nat).(let TMP_14 \def (Flat Appl) in (let
349 TMP_15 \def (TLRef i) in (let TMP_16 \def (THeads TMP_14 ws TMP_15) in (eq T
350 t TMP_16)))))) in (let TMP_18 \def (\lambda (ws: TList).(\lambda (_:
351 nat).(nfs2 c ws))) in (let TMP_20 \def (\lambda (_: TList).(\lambda (i:
352 nat).(let TMP_19 \def (TLRef i) in (nf2 c TMP_19)))) in (let TMP_21 \def
353 (ex3_2 TList nat TMP_17 TMP_18 TMP_20) in (let TMP_24 \def (\lambda (v:
354 T).(\lambda (_: T).(let TMP_22 \def (Bind Abst) in (let TMP_23 \def (THead
355 TMP_22 w v) in (eq T t TMP_23))))) in (let TMP_25 \def (\lambda (_:
356 T).(\lambda (w0: T).(ty3 g c w w0))) in (let TMP_28 \def (\lambda (v:
357 T).(\lambda (_: T).(let TMP_26 \def (Bind Abst) in (let TMP_27 \def (CHead c
358 TMP_26 w) in (ty3 g TMP_27 v u))))) in (let TMP_31 \def (\lambda (v:
359 T).(\lambda (_: T).(let TMP_29 \def (Bind Abst) in (let TMP_30 \def (CHead c
360 TMP_29 w) in (nf2 TMP_30 v))))) in (let TMP_32 \def (ex4_2 T T TMP_24 TMP_25
361 TMP_28 TMP_31) in (let TMP_199 \def (\lambda (H4: (ex3_2 T T (\lambda (w0:
362 T).(\lambda (u0: T).(eq T t (THead (Bind Abst) w0 u0)))) (\lambda (w0:
363 T).(\lambda (_: T).(nf2 c w0))) (\lambda (w0: T).(\lambda (u0: T).(nf2 (CHead
364 c (Bind Abst) w0) u0))))).(let TMP_35 \def (\lambda (w0: T).(\lambda (u0:
365 T).(let TMP_33 \def (Bind Abst) in (let TMP_34 \def (THead TMP_33 w0 u0) in
366 (eq T t TMP_34))))) in (let TMP_36 \def (\lambda (w0: T).(\lambda (_: T).(nf2
367 c w0))) in (let TMP_39 \def (\lambda (w0: T).(\lambda (u0: T).(let TMP_37
368 \def (Bind Abst) in (let TMP_38 \def (CHead c TMP_37 w0) in (nf2 TMP_38
369 u0))))) in (let TMP_42 \def (\lambda (v: T).(\lambda (_: T).(let TMP_40 \def
370 (Bind Abst) in (let TMP_41 \def (THead TMP_40 w v) in (eq T t TMP_41))))) in
371 (let TMP_43 \def (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) in (let
372 TMP_46 \def (\lambda (v: T).(\lambda (_: T).(let TMP_44 \def (Bind Abst) in
373 (let TMP_45 \def (CHead c TMP_44 w) in (ty3 g TMP_45 v u))))) in (let TMP_49
374 \def (\lambda (v: T).(\lambda (_: T).(let TMP_47 \def (Bind Abst) in (let
375 TMP_48 \def (CHead c TMP_47 w) in (nf2 TMP_48 v))))) in (let TMP_50 \def
376 (ex4_2 T T TMP_42 TMP_43 TMP_46 TMP_49) in (let TMP_198 \def (\lambda (x0:
377 T).(\lambda (x1: T).(\lambda (H5: (eq T t (THead (Bind Abst) x0
378 x1))).(\lambda (H6: (nf2 c x0)).(\lambda (H7: (nf2 (CHead c (Bind Abst) x0)
379 x1)).(let TMP_53 \def (\lambda (t0: T).(let TMP_51 \def (Bind Abst) in (let
380 TMP_52 \def (THead TMP_51 w u) in (ty3 g c t0 TMP_52)))) in (let TMP_54 \def
381 (Bind Abst) in (let TMP_55 \def (THead TMP_54 x0 x1) in (let H8 \def (eq_ind
382 T t TMP_53 H TMP_55 H5) in (let TMP_56 \def (Bind Abst) in (let TMP_57 \def
383 (THead TMP_56 x0 x1) in (let TMP_68 \def (\lambda (t0: T).(let TMP_60 \def
384 (\lambda (v: T).(\lambda (_: T).(let TMP_58 \def (Bind Abst) in (let TMP_59
385 \def (THead TMP_58 w v) in (eq T t0 TMP_59))))) in (let TMP_61 \def (\lambda
386 (_: T).(\lambda (w0: T).(ty3 g c w w0))) in (let TMP_64 \def (\lambda (v:
387 T).(\lambda (_: T).(let TMP_62 \def (Bind Abst) in (let TMP_63 \def (CHead c
388 TMP_62 w) in (ty3 g TMP_63 v u))))) in (let TMP_67 \def (\lambda (v:
389 T).(\lambda (_: T).(let TMP_65 \def (Bind Abst) in (let TMP_66 \def (CHead c
390 TMP_65 w) in (nf2 TMP_66 v))))) in (ex4_2 T T TMP_60 TMP_61 TMP_64
391 TMP_67)))))) in (let TMP_71 \def (\lambda (t0: T).(let TMP_69 \def (Bind
392 Abst) in (let TMP_70 \def (THead TMP_69 w u) in (ty3 g c TMP_70 t0)))) in
393 (let TMP_76 \def (\lambda (v: T).(\lambda (_: T).(let TMP_72 \def (Bind Abst)
394 in (let TMP_73 \def (THead TMP_72 x0 x1) in (let TMP_74 \def (Bind Abst) in
395 (let TMP_75 \def (THead TMP_74 w v) in (eq T TMP_73 TMP_75))))))) in (let
396 TMP_77 \def (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) in (let TMP_80
397 \def (\lambda (v: T).(\lambda (_: T).(let TMP_78 \def (Bind Abst) in (let
398 TMP_79 \def (CHead c TMP_78 w) in (ty3 g TMP_79 v u))))) in (let TMP_83 \def
399 (\lambda (v: T).(\lambda (_: T).(let TMP_81 \def (Bind Abst) in (let TMP_82
400 \def (CHead c TMP_81 w) in (nf2 TMP_82 v))))) in (let TMP_84 \def (ex4_2 T T
401 TMP_76 TMP_77 TMP_80 TMP_83) in (let TMP_191 \def (\lambda (x: T).(\lambda
402 (H9: (ty3 g c (THead (Bind Abst) w u) x)).(let TMP_87 \def (\lambda (t2:
403 T).(\lambda (_: T).(let TMP_85 \def (Bind Abst) in (let TMP_86 \def (THead
404 TMP_85 w t2) in (pc3 c TMP_86 x))))) in (let TMP_88 \def (\lambda (_:
405 T).(\lambda (t0: T).(ty3 g c w t0))) in (let TMP_91 \def (\lambda (t2:
406 T).(\lambda (_: T).(let TMP_89 \def (Bind Abst) in (let TMP_90 \def (CHead c
407 TMP_89 w) in (ty3 g TMP_90 u t2))))) in (let TMP_96 \def (\lambda (v:
408 T).(\lambda (_: T).(let TMP_92 \def (Bind Abst) in (let TMP_93 \def (THead
409 TMP_92 x0 x1) in (let TMP_94 \def (Bind Abst) in (let TMP_95 \def (THead
410 TMP_94 w v) in (eq T TMP_93 TMP_95))))))) in (let TMP_97 \def (\lambda (_:
411 T).(\lambda (w0: T).(ty3 g c w w0))) in (let TMP_100 \def (\lambda (v:
412 T).(\lambda (_: T).(let TMP_98 \def (Bind Abst) in (let TMP_99 \def (CHead c
413 TMP_98 w) in (ty3 g TMP_99 v u))))) in (let TMP_103 \def (\lambda (v:
414 T).(\lambda (_: T).(let TMP_101 \def (Bind Abst) in (let TMP_102 \def (CHead
415 c TMP_101 w) in (nf2 TMP_102 v))))) in (let TMP_104 \def (ex4_2 T T TMP_96
416 TMP_97 TMP_100 TMP_103) in (let TMP_189 \def (\lambda (x2: T).(\lambda (x3:
417 T).(\lambda (_: (pc3 c (THead (Bind Abst) w x2) x)).(\lambda (H11: (ty3 g c w
418 x3)).(\lambda (H12: (ty3 g (CHead c (Bind Abst) w) u x2)).(let TMP_109 \def
419 (\lambda (t2: T).(\lambda (_: T).(let TMP_105 \def (Bind Abst) in (let
420 TMP_106 \def (THead TMP_105 x0 t2) in (let TMP_107 \def (Bind Abst) in (let
421 TMP_108 \def (THead TMP_107 w u) in (pc3 c TMP_106 TMP_108))))))) in (let
422 TMP_110 \def (\lambda (_: T).(\lambda (t0: T).(ty3 g c x0 t0))) in (let
423 TMP_113 \def (\lambda (t2: T).(\lambda (_: T).(let TMP_111 \def (Bind Abst)
424 in (let TMP_112 \def (CHead c TMP_111 x0) in (ty3 g TMP_112 x1 t2))))) in
425 (let TMP_118 \def (\lambda (v: T).(\lambda (_: T).(let TMP_114 \def (Bind
426 Abst) in (let TMP_115 \def (THead TMP_114 x0 x1) in (let TMP_116 \def (Bind
427 Abst) in (let TMP_117 \def (THead TMP_116 w v) in (eq T TMP_115
428 TMP_117))))))) in (let TMP_119 \def (\lambda (_: T).(\lambda (w0: T).(ty3 g c
429 w w0))) in (let TMP_122 \def (\lambda (v: T).(\lambda (_: T).(let TMP_120
430 \def (Bind Abst) in (let TMP_121 \def (CHead c TMP_120 w) in (ty3 g TMP_121 v
431 u))))) in (let TMP_125 \def (\lambda (v: T).(\lambda (_: T).(let TMP_123 \def
432 (Bind Abst) in (let TMP_124 \def (CHead c TMP_123 w) in (nf2 TMP_124 v)))))
433 in (let TMP_126 \def (ex4_2 T T TMP_118 TMP_119 TMP_122 TMP_125) in (let
434 TMP_185 \def (\lambda (x4: T).(\lambda (x5: T).(\lambda (H13: (pc3 c (THead
435 (Bind Abst) x0 x4) (THead (Bind Abst) w u))).(\lambda (_: (ty3 g c x0
436 x5)).(\lambda (H15: (ty3 g (CHead c (Bind Abst) x0) x1 x4)).(let TMP_127 \def
437 (pc3 c x0 w) in (let TMP_130 \def (\forall (b: B).(\forall (u0: T).(let
438 TMP_128 \def (Bind b) in (let TMP_129 \def (CHead c TMP_128 u0) in (pc3
439 TMP_129 x4 u))))) in (let TMP_135 \def (\lambda (v: T).(\lambda (_: T).(let
440 TMP_131 \def (Bind Abst) in (let TMP_132 \def (THead TMP_131 x0 x1) in (let
441 TMP_133 \def (Bind Abst) in (let TMP_134 \def (THead TMP_133 w v) in (eq T
442 TMP_132 TMP_134))))))) in (let TMP_136 \def (\lambda (_: T).(\lambda (w0:
443 T).(ty3 g c w w0))) in (let TMP_139 \def (\lambda (v: T).(\lambda (_: T).(let
444 TMP_137 \def (Bind Abst) in (let TMP_138 \def (CHead c TMP_137 w) in (ty3 g
445 TMP_138 v u))))) in (let TMP_142 \def (\lambda (v: T).(\lambda (_: T).(let
446 TMP_140 \def (Bind Abst) in (let TMP_141 \def (CHead c TMP_140 w) in (nf2
447 TMP_141 v))))) in (let TMP_143 \def (ex4_2 T T TMP_135 TMP_136 TMP_139
448 TMP_142) in (let TMP_183 \def (\lambda (H16: (pc3 c x0 w)).(\lambda (H17:
449 ((\forall (b: B).(\forall (u0: T).(pc3 (CHead c (Bind b) u0) x4 u))))).(let
450 H_y \def (pc3_nf2 c x0 w H16 H6 H1) in (let TMP_146 \def (\lambda (t0:
451 T).(let TMP_144 \def (Bind Abst) in (let TMP_145 \def (CHead c TMP_144 t0) in
452 (ty3 g TMP_145 x1 x4)))) in (let H18 \def (eq_ind T x0 TMP_146 H15 w H_y) in
453 (let TMP_149 \def (\lambda (t0: T).(let TMP_147 \def (Bind Abst) in (let
454 TMP_148 \def (CHead c TMP_147 t0) in (nf2 TMP_148 x1)))) in (let H19 \def
455 (eq_ind T x0 TMP_149 H7 w H_y) in (let TMP_162 \def (\lambda (t0: T).(let
456 TMP_154 \def (\lambda (v: T).(\lambda (_: T).(let TMP_150 \def (Bind Abst) in
457 (let TMP_151 \def (THead TMP_150 t0 x1) in (let TMP_152 \def (Bind Abst) in
458 (let TMP_153 \def (THead TMP_152 w v) in (eq T TMP_151 TMP_153))))))) in (let
459 TMP_155 \def (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) in (let
460 TMP_158 \def (\lambda (v: T).(\lambda (_: T).(let TMP_156 \def (Bind Abst) in
461 (let TMP_157 \def (CHead c TMP_156 w) in (ty3 g TMP_157 v u))))) in (let
462 TMP_161 \def (\lambda (v: T).(\lambda (_: T).(let TMP_159 \def (Bind Abst) in
463 (let TMP_160 \def (CHead c TMP_159 w) in (nf2 TMP_160 v))))) in (ex4_2 T T
464 TMP_154 TMP_155 TMP_158 TMP_161)))))) in (let TMP_167 \def (\lambda (v:
465 T).(\lambda (_: T).(let TMP_163 \def (Bind Abst) in (let TMP_164 \def (THead
466 TMP_163 w x1) in (let TMP_165 \def (Bind Abst) in (let TMP_166 \def (THead
467 TMP_165 w v) in (eq T TMP_164 TMP_166))))))) in (let TMP_168 \def (\lambda
468 (_: T).(\lambda (w0: T).(ty3 g c w w0))) in (let TMP_171 \def (\lambda (v:
469 T).(\lambda (_: T).(let TMP_169 \def (Bind Abst) in (let TMP_170 \def (CHead
470 c TMP_169 w) in (ty3 g TMP_170 v u))))) in (let TMP_174 \def (\lambda (v:
471 T).(\lambda (_: T).(let TMP_172 \def (Bind Abst) in (let TMP_173 \def (CHead
472 c TMP_172 w) in (nf2 TMP_173 v))))) in (let TMP_175 \def (Bind Abst) in (let
473 TMP_176 \def (THead TMP_175 w x1) in (let TMP_177 \def (refl_equal T TMP_176)
474 in (let TMP_178 \def (Bind Abst) in (let TMP_179 \def (CHead c TMP_178 w) in
475 (let TMP_180 \def (H17 Abst w) in (let TMP_181 \def (ty3_conv g TMP_179 u x2
476 H12 x1 x4 H18 TMP_180) in (let TMP_182 \def (ex4_2_intro T T TMP_167 TMP_168
477 TMP_171 TMP_174 x1 x3 TMP_177 H11 TMP_181 H19) in (eq_ind_r T w TMP_162
478 TMP_182 x0 H_y))))))))))))))))))))) in (let TMP_184 \def (pc3_gen_abst c x0 w
479 x4 u H13) in (land_ind TMP_127 TMP_130 TMP_143 TMP_183 TMP_184)))))))))))))))
480 in (let TMP_186 \def (Bind Abst) in (let TMP_187 \def (THead TMP_186 w u) in
481 (let TMP_188 \def (ty3_gen_bind g Abst c x0 x1 TMP_187 H8) in (ex3_2_ind T T
482 TMP_109 TMP_110 TMP_113 TMP_126 TMP_185 TMP_188)))))))))))))))))) in (let
483 TMP_190 \def (ty3_gen_bind g Abst c w u x H9) in (ex3_2_ind T T TMP_87 TMP_88
484 TMP_91 TMP_104 TMP_189 TMP_190))))))))))))) in (let TMP_192 \def (Bind Abst)
485 in (let TMP_193 \def (THead TMP_192 x0 x1) in (let TMP_194 \def (Bind Abst)
486 in (let TMP_195 \def (THead TMP_194 w u) in (let TMP_196 \def (ty3_correct g
487 c TMP_193 TMP_195 H8) in (let TMP_197 \def (ex_ind T TMP_71 TMP_84 TMP_191
488 TMP_196) in (eq_ind_r T TMP_57 TMP_68 TMP_197 t H5))))))))))))))))))))))))))
489 in (ex3_2_ind T T TMP_35 TMP_36 TMP_39 TMP_50 TMP_198 H4))))))))))) in (let
490 TMP_247 \def (\lambda (H4: (ex nat (\lambda (n: nat).(eq T t (TSort
491 n))))).(let TMP_201 \def (\lambda (n: nat).(let TMP_200 \def (TSort n) in (eq
492 T t TMP_200))) in (let TMP_204 \def (\lambda (v: T).(\lambda (_: T).(let
493 TMP_202 \def (Bind Abst) in (let TMP_203 \def (THead TMP_202 w v) in (eq T t
494 TMP_203))))) in (let TMP_205 \def (\lambda (_: T).(\lambda (w0: T).(ty3 g c w
495 w0))) in (let TMP_208 \def (\lambda (v: T).(\lambda (_: T).(let TMP_206 \def
496 (Bind Abst) in (let TMP_207 \def (CHead c TMP_206 w) in (ty3 g TMP_207 v
497 u))))) in (let TMP_211 \def (\lambda (v: T).(\lambda (_: T).(let TMP_209 \def
498 (Bind Abst) in (let TMP_210 \def (CHead c TMP_209 w) in (nf2 TMP_210 v)))))
499 in (let TMP_212 \def (ex4_2 T T TMP_204 TMP_205 TMP_208 TMP_211) in (let
500 TMP_246 \def (\lambda (x: nat).(\lambda (H5: (eq T t (TSort x))).(let TMP_215
501 \def (\lambda (t0: T).(let TMP_213 \def (Bind Abst) in (let TMP_214 \def
502 (THead TMP_213 w u) in (ty3 g c t0 TMP_214)))) in (let TMP_216 \def (TSort x)
503 in (let H6 \def (eq_ind T t TMP_215 H TMP_216 H5) in (let TMP_217 \def (TSort
504 x) in (let TMP_228 \def (\lambda (t0: T).(let TMP_220 \def (\lambda (v:
505 T).(\lambda (_: T).(let TMP_218 \def (Bind Abst) in (let TMP_219 \def (THead
506 TMP_218 w v) in (eq T t0 TMP_219))))) in (let TMP_221 \def (\lambda (_:
507 T).(\lambda (w0: T).(ty3 g c w w0))) in (let TMP_224 \def (\lambda (v:
508 T).(\lambda (_: T).(let TMP_222 \def (Bind Abst) in (let TMP_223 \def (CHead
509 c TMP_222 w) in (ty3 g TMP_223 v u))))) in (let TMP_227 \def (\lambda (v:
510 T).(\lambda (_: T).(let TMP_225 \def (Bind Abst) in (let TMP_226 \def (CHead
511 c TMP_225 w) in (nf2 TMP_226 v))))) in (ex4_2 T T TMP_220 TMP_221 TMP_224
512 TMP_227)))))) in (let TMP_229 \def (next g x) in (let TMP_230 \def (Bind
513 Abst) in (let TMP_231 \def (THead TMP_230 w u) in (let TMP_232 \def
514 (ty3_gen_sort g c TMP_231 x H6) in (let TMP_236 \def (\lambda (v: T).(\lambda
515 (_: T).(let TMP_233 \def (TSort x) in (let TMP_234 \def (Bind Abst) in (let
516 TMP_235 \def (THead TMP_234 w v) in (eq T TMP_233 TMP_235)))))) in (let
517 TMP_237 \def (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) in (let
518 TMP_240 \def (\lambda (v: T).(\lambda (_: T).(let TMP_238 \def (Bind Abst) in
519 (let TMP_239 \def (CHead c TMP_238 w) in (ty3 g TMP_239 v u))))) in (let
520 TMP_243 \def (\lambda (v: T).(\lambda (_: T).(let TMP_241 \def (Bind Abst) in
521 (let TMP_242 \def (CHead c TMP_241 w) in (nf2 TMP_242 v))))) in (let TMP_244
522 \def (ex4_2 T T TMP_236 TMP_237 TMP_240 TMP_243) in (let TMP_245 \def
523 (pc3_gen_sort_abst c w u TMP_229 TMP_232 TMP_244) in (eq_ind_r T TMP_217
524 TMP_228 TMP_245 t H5)))))))))))))))))) in (ex_ind nat TMP_201 TMP_212 TMP_246
525 H4))))))))) in (let TMP_570 \def (\lambda (H4: (ex3_2 TList nat (\lambda (ws:
526 TList).(\lambda (i: nat).(eq T t (THeads (Flat Appl) ws (TLRef i)))))
527 (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_:
528 TList).(\lambda (i: nat).(nf2 c (TLRef i)))))).(let TMP_251 \def (\lambda
529 (ws: TList).(\lambda (i: nat).(let TMP_248 \def (Flat Appl) in (let TMP_249
530 \def (TLRef i) in (let TMP_250 \def (THeads TMP_248 ws TMP_249) in (eq T t
531 TMP_250)))))) in (let TMP_252 \def (\lambda (ws: TList).(\lambda (_:
532 nat).(nfs2 c ws))) in (let TMP_254 \def (\lambda (_: TList).(\lambda (i:
533 nat).(let TMP_253 \def (TLRef i) in (nf2 c TMP_253)))) in (let TMP_257 \def
534 (\lambda (v: T).(\lambda (_: T).(let TMP_255 \def (Bind Abst) in (let TMP_256
535 \def (THead TMP_255 w v) in (eq T t TMP_256))))) in (let TMP_258 \def
536 (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) in (let TMP_261 \def
537 (\lambda (v: T).(\lambda (_: T).(let TMP_259 \def (Bind Abst) in (let TMP_260
538 \def (CHead c TMP_259 w) in (ty3 g TMP_260 v u))))) in (let TMP_264 \def
539 (\lambda (v: T).(\lambda (_: T).(let TMP_262 \def (Bind Abst) in (let TMP_263
540 \def (CHead c TMP_262 w) in (nf2 TMP_263 v))))) in (let TMP_265 \def (ex4_2 T
541 T TMP_257 TMP_258 TMP_261 TMP_264) in (let TMP_569 \def (\lambda (x0:
542 TList).(\lambda (x1: nat).(\lambda (H5: (eq T t (THeads (Flat Appl) x0 (TLRef
543 x1)))).(\lambda (_: (nfs2 c x0)).(\lambda (H7: (nf2 c (TLRef x1))).(let
544 TMP_268 \def (\lambda (t0: T).(let TMP_266 \def (Bind Abst) in (let TMP_267
545 \def (THead TMP_266 w u) in (ty3 g c t0 TMP_267)))) in (let TMP_269 \def
546 (Flat Appl) in (let TMP_270 \def (TLRef x1) in (let TMP_271 \def (THeads
547 TMP_269 x0 TMP_270) in (let H8 \def (eq_ind T t TMP_268 H TMP_271 H5) in (let
548 TMP_272 \def (Flat Appl) in (let TMP_273 \def (TLRef x1) in (let TMP_274 \def
549 (THeads TMP_272 x0 TMP_273) in (let TMP_285 \def (\lambda (t0: T).(let
550 TMP_277 \def (\lambda (v: T).(\lambda (_: T).(let TMP_275 \def (Bind Abst) in
551 (let TMP_276 \def (THead TMP_275 w v) in (eq T t0 TMP_276))))) in (let
552 TMP_278 \def (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) in (let
553 TMP_281 \def (\lambda (v: T).(\lambda (_: T).(let TMP_279 \def (Bind Abst) in
554 (let TMP_280 \def (CHead c TMP_279 w) in (ty3 g TMP_280 v u))))) in (let
555 TMP_284 \def (\lambda (v: T).(\lambda (_: T).(let TMP_282 \def (Bind Abst) in
556 (let TMP_283 \def (CHead c TMP_282 w) in (nf2 TMP_283 v))))) in (ex4_2 T T
557 TMP_277 TMP_278 TMP_281 TMP_284)))))) in (let H9 \def H2 in (let H10 \def H8
558 in (let TMP_299 \def (\lambda (t0: T).((ty3 g c (THeads (Flat Appl) x0 (TLRef
559 x1)) (THead (Bind Abst) w t0)) \to ((ty3_nf2_inv_abst_premise c w t0) \to
560 (let TMP_291 \def (\lambda (v: T).(\lambda (_: T).(let TMP_286 \def (Flat
561 Appl) in (let TMP_287 \def (TLRef x1) in (let TMP_288 \def (THeads TMP_286 x0
562 TMP_287) in (let TMP_289 \def (Bind Abst) in (let TMP_290 \def (THead TMP_289
563 w v) in (eq T TMP_288 TMP_290)))))))) in (let TMP_292 \def (\lambda (_:
564 T).(\lambda (w0: T).(ty3 g c w w0))) in (let TMP_295 \def (\lambda (v:
565 T).(\lambda (_: T).(let TMP_293 \def (Bind Abst) in (let TMP_294 \def (CHead
566 c TMP_293 w) in (ty3 g TMP_294 v t0))))) in (let TMP_298 \def (\lambda (v:
567 T).(\lambda (_: T).(let TMP_296 \def (Bind Abst) in (let TMP_297 \def (CHead
568 c TMP_296 w) in (nf2 TMP_297 v))))) in (ex4_2 T T TMP_291 TMP_292 TMP_295
569 TMP_298)))))))) in (let TMP_313 \def (\lambda (t0: T).(\forall (x: T).((ty3 g
570 c (THeads (Flat Appl) x0 (TLRef x1)) (THead (Bind Abst) t0 x)) \to
571 ((ty3_nf2_inv_abst_premise c t0 x) \to (let TMP_305 \def (\lambda (v:
572 T).(\lambda (_: T).(let TMP_300 \def (Flat Appl) in (let TMP_301 \def (TLRef
573 x1) in (let TMP_302 \def (THeads TMP_300 x0 TMP_301) in (let TMP_303 \def
574 (Bind Abst) in (let TMP_304 \def (THead TMP_303 t0 v) in (eq T TMP_302
575 TMP_304)))))))) in (let TMP_306 \def (\lambda (_: T).(\lambda (w0: T).(ty3 g
576 c t0 w0))) in (let TMP_309 \def (\lambda (v: T).(\lambda (_: T).(let TMP_307
577 \def (Bind Abst) in (let TMP_308 \def (CHead c TMP_307 t0) in (ty3 g TMP_308
578 v x))))) in (let TMP_312 \def (\lambda (v: T).(\lambda (_: T).(let TMP_310
579 \def (Bind Abst) in (let TMP_311 \def (CHead c TMP_310 t0) in (nf2 TMP_311
580 v))))) in (ex4_2 T T TMP_305 TMP_306 TMP_309 TMP_312))))))))) in (let TMP_327
581 \def (\lambda (t0: TList).(\forall (x: T).(\forall (x2: T).((ty3 g c (THeads
582 (Flat Appl) t0 (TLRef x1)) (THead (Bind Abst) x x2)) \to
583 ((ty3_nf2_inv_abst_premise c x x2) \to (let TMP_319 \def (\lambda (v:
584 T).(\lambda (_: T).(let TMP_314 \def (Flat Appl) in (let TMP_315 \def (TLRef
585 x1) in (let TMP_316 \def (THeads TMP_314 t0 TMP_315) in (let TMP_317 \def
586 (Bind Abst) in (let TMP_318 \def (THead TMP_317 x v) in (eq T TMP_316
587 TMP_318)))))))) in (let TMP_320 \def (\lambda (_: T).(\lambda (w0: T).(ty3 g
588 c x w0))) in (let TMP_323 \def (\lambda (v: T).(\lambda (_: T).(let TMP_321
589 \def (Bind Abst) in (let TMP_322 \def (CHead c TMP_321 x) in (ty3 g TMP_322 v
590 x2))))) in (let TMP_326 \def (\lambda (v: T).(\lambda (_: T).(let TMP_324
591 \def (Bind Abst) in (let TMP_325 \def (CHead c TMP_324 x) in (nf2 TMP_325
592 v))))) in (ex4_2 T T TMP_319 TMP_320 TMP_323 TMP_326)))))))))) in (let
593 TMP_433 \def (\lambda (x: T).(\lambda (x2: T).(\lambda (H11: (ty3 g c (TLRef
594 x1) (THead (Bind Abst) x x2))).(\lambda (H12: (ty3_nf2_inv_abst_premise c x
595 x2)).(let TMP_332 \def (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(let
596 TMP_328 \def (S x1) in (let TMP_329 \def (lift TMP_328 O t0) in (let TMP_330
597 \def (Bind Abst) in (let TMP_331 \def (THead TMP_330 x x2) in (pc3 c TMP_329
598 TMP_331)))))))) in (let TMP_335 \def (\lambda (e: C).(\lambda (u0:
599 T).(\lambda (_: T).(let TMP_333 \def (Bind Abbr) in (let TMP_334 \def (CHead
600 e TMP_333 u0) in (getl x1 c TMP_334)))))) in (let TMP_336 \def (\lambda (e:
601 C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0)))) in (let TMP_337 \def
602 (ex3_3 C T T TMP_332 TMP_335 TMP_336) in (let TMP_342 \def (\lambda (_:
603 C).(\lambda (u0: T).(\lambda (_: T).(let TMP_338 \def (S x1) in (let TMP_339
604 \def (lift TMP_338 O u0) in (let TMP_340 \def (Bind Abst) in (let TMP_341
605 \def (THead TMP_340 x x2) in (pc3 c TMP_339 TMP_341)))))))) in (let TMP_345
606 \def (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(let TMP_343 \def (Bind
607 Abst) in (let TMP_344 \def (CHead e TMP_343 u0) in (getl x1 c TMP_344))))))
608 in (let TMP_346 \def (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g
609 e u0 t0)))) in (let TMP_347 \def (ex3_3 C T T TMP_342 TMP_345 TMP_346) in
610 (let TMP_351 \def (\lambda (v: T).(\lambda (_: T).(let TMP_348 \def (TLRef
611 x1) in (let TMP_349 \def (Bind Abst) in (let TMP_350 \def (THead TMP_349 x v)
612 in (eq T TMP_348 TMP_350)))))) in (let TMP_352 \def (\lambda (_: T).(\lambda
613 (w0: T).(ty3 g c x w0))) in (let TMP_355 \def (\lambda (v: T).(\lambda (_:
614 T).(let TMP_353 \def (Bind Abst) in (let TMP_354 \def (CHead c TMP_353 x) in
615 (ty3 g TMP_354 v x2))))) in (let TMP_358 \def (\lambda (v: T).(\lambda (_:
616 T).(let TMP_356 \def (Bind Abst) in (let TMP_357 \def (CHead c TMP_356 x) in
617 (nf2 TMP_357 v))))) in (let TMP_359 \def (ex4_2 T T TMP_351 TMP_352 TMP_355
618 TMP_358) in (let TMP_394 \def (\lambda (H13: (ex3_3 C T T (\lambda (_:
619 C).(\lambda (_: T).(\lambda (t0: T).(pc3 c (lift (S x1) O t0) (THead (Bind
620 Abst) x x2))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl x1 c
621 (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0:
622 T).(ty3 g e u0 t0)))))).(let TMP_364 \def (\lambda (_: C).(\lambda (_:
623 T).(\lambda (t0: T).(let TMP_360 \def (S x1) in (let TMP_361 \def (lift
624 TMP_360 O t0) in (let TMP_362 \def (Bind Abst) in (let TMP_363 \def (THead
625 TMP_362 x x2) in (pc3 c TMP_361 TMP_363)))))))) in (let TMP_367 \def (\lambda
626 (e: C).(\lambda (u0: T).(\lambda (_: T).(let TMP_365 \def (Bind Abbr) in (let
627 TMP_366 \def (CHead e TMP_365 u0) in (getl x1 c TMP_366)))))) in (let TMP_368
628 \def (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0)))) in
629 (let TMP_372 \def (\lambda (v: T).(\lambda (_: T).(let TMP_369 \def (TLRef
630 x1) in (let TMP_370 \def (Bind Abst) in (let TMP_371 \def (THead TMP_370 x v)
631 in (eq T TMP_369 TMP_371)))))) in (let TMP_373 \def (\lambda (_: T).(\lambda
632 (w0: T).(ty3 g c x w0))) in (let TMP_376 \def (\lambda (v: T).(\lambda (_:
633 T).(let TMP_374 \def (Bind Abst) in (let TMP_375 \def (CHead c TMP_374 x) in
634 (ty3 g TMP_375 v x2))))) in (let TMP_379 \def (\lambda (v: T).(\lambda (_:
635 T).(let TMP_377 \def (Bind Abst) in (let TMP_378 \def (CHead c TMP_377 x) in
636 (nf2 TMP_378 v))))) in (let TMP_380 \def (ex4_2 T T TMP_372 TMP_373 TMP_376
637 TMP_379) in (let TMP_393 \def (\lambda (x3: C).(\lambda (x4: T).(\lambda (x5:
638 T).(\lambda (_: (pc3 c (lift (S x1) O x5) (THead (Bind Abst) x x2))).(\lambda
639 (H15: (getl x1 c (CHead x3 (Bind Abbr) x4))).(\lambda (_: (ty3 g x3 x4
640 x5)).(let TMP_384 \def (\lambda (v: T).(\lambda (_: T).(let TMP_381 \def
641 (TLRef x1) in (let TMP_382 \def (Bind Abst) in (let TMP_383 \def (THead
642 TMP_382 x v) in (eq T TMP_381 TMP_383)))))) in (let TMP_385 \def (\lambda (_:
643 T).(\lambda (w0: T).(ty3 g c x w0))) in (let TMP_388 \def (\lambda (v:
644 T).(\lambda (_: T).(let TMP_386 \def (Bind Abst) in (let TMP_387 \def (CHead
645 c TMP_386 x) in (ty3 g TMP_387 v x2))))) in (let TMP_391 \def (\lambda (v:
646 T).(\lambda (_: T).(let TMP_389 \def (Bind Abst) in (let TMP_390 \def (CHead
647 c TMP_389 x) in (nf2 TMP_390 v))))) in (let TMP_392 \def (ex4_2 T T TMP_384
648 TMP_385 TMP_388 TMP_391) in (nf2_gen_lref c x3 x4 x1 H15 H7
649 TMP_392)))))))))))) in (ex3_3_ind C T T TMP_364 TMP_367 TMP_368 TMP_380
650 TMP_393 H13))))))))))) in (let TMP_429 \def (\lambda (H13: (ex3_3 C T T
651 (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 c (lift (S x1) O u0)
652 (THead (Bind Abst) x x2))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
653 T).(getl x1 c (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0:
654 T).(\lambda (t0: T).(ty3 g e u0 t0)))))).(let TMP_399 \def (\lambda (_:
655 C).(\lambda (u0: T).(\lambda (_: T).(let TMP_395 \def (S x1) in (let TMP_396
656 \def (lift TMP_395 O u0) in (let TMP_397 \def (Bind Abst) in (let TMP_398
657 \def (THead TMP_397 x x2) in (pc3 c TMP_396 TMP_398)))))))) in (let TMP_402
658 \def (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(let TMP_400 \def (Bind
659 Abst) in (let TMP_401 \def (CHead e TMP_400 u0) in (getl x1 c TMP_401))))))
660 in (let TMP_403 \def (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g
661 e u0 t0)))) in (let TMP_407 \def (\lambda (v: T).(\lambda (_: T).(let TMP_404
662 \def (TLRef x1) in (let TMP_405 \def (Bind Abst) in (let TMP_406 \def (THead
663 TMP_405 x v) in (eq T TMP_404 TMP_406)))))) in (let TMP_408 \def (\lambda (_:
664 T).(\lambda (w0: T).(ty3 g c x w0))) in (let TMP_411 \def (\lambda (v:
665 T).(\lambda (_: T).(let TMP_409 \def (Bind Abst) in (let TMP_410 \def (CHead
666 c TMP_409 x) in (ty3 g TMP_410 v x2))))) in (let TMP_414 \def (\lambda (v:
667 T).(\lambda (_: T).(let TMP_412 \def (Bind Abst) in (let TMP_413 \def (CHead
668 c TMP_412 x) in (nf2 TMP_413 v))))) in (let TMP_415 \def (ex4_2 T T TMP_407
669 TMP_408 TMP_411 TMP_414) in (let TMP_428 \def (\lambda (x3: C).(\lambda (x4:
670 T).(\lambda (x5: T).(\lambda (H14: (pc3 c (lift (S x1) O x4) (THead (Bind
671 Abst) x x2))).(\lambda (H15: (getl x1 c (CHead x3 (Bind Abst) x4))).(\lambda
672 (_: (ty3 g x3 x4 x5)).(let H_x0 \def (H12 x3 x4 x1 H15 TNil H14) in (let H17
673 \def H_x0 in (let TMP_419 \def (\lambda (v: T).(\lambda (_: T).(let TMP_416
674 \def (TLRef x1) in (let TMP_417 \def (Bind Abst) in (let TMP_418 \def (THead
675 TMP_417 x v) in (eq T TMP_416 TMP_418)))))) in (let TMP_420 \def (\lambda (_:
676 T).(\lambda (w0: T).(ty3 g c x w0))) in (let TMP_423 \def (\lambda (v:
677 T).(\lambda (_: T).(let TMP_421 \def (Bind Abst) in (let TMP_422 \def (CHead
678 c TMP_421 x) in (ty3 g TMP_422 v x2))))) in (let TMP_426 \def (\lambda (v:
679 T).(\lambda (_: T).(let TMP_424 \def (Bind Abst) in (let TMP_425 \def (CHead
680 c TMP_424 x) in (nf2 TMP_425 v))))) in (let TMP_427 \def (ex4_2 T T TMP_419
681 TMP_420 TMP_423 TMP_426) in (False_ind TMP_427 H17)))))))))))))) in
682 (ex3_3_ind C T T TMP_399 TMP_402 TMP_403 TMP_415 TMP_428 H13))))))))))) in
683 (let TMP_430 \def (Bind Abst) in (let TMP_431 \def (THead TMP_430 x x2) in
684 (let TMP_432 \def (ty3_gen_lref g c TMP_431 x1 H11) in (or_ind TMP_337
685 TMP_347 TMP_359 TMP_394 TMP_429 TMP_432))))))))))))))))))))))) in (let
686 TMP_564 \def (\lambda (t0: T).(\lambda (t1: TList).(\lambda (H11: ((\forall
687 (x: T).(\forall (x2: T).((ty3 g c (THeads (Flat Appl) t1 (TLRef x1)) (THead
688 (Bind Abst) x x2)) \to ((ty3_nf2_inv_abst_premise c x x2) \to (ex4_2 T T
689 (\lambda (v: T).(\lambda (_: T).(eq T (THeads (Flat Appl) t1 (TLRef x1))
690 (THead (Bind Abst) x v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c x w0)))
691 (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) x) v x2)))
692 (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) x)
693 v)))))))))).(\lambda (x: T).(\lambda (x2: T).(\lambda (H12: (ty3 g c (THead
694 (Flat Appl) t0 (THeads (Flat Appl) t1 (TLRef x1))) (THead (Bind Abst) x
695 x2))).(\lambda (H13: (ty3_nf2_inv_abst_premise c x x2)).(let TMP_440 \def
696 (\lambda (u0: T).(\lambda (t2: T).(let TMP_434 \def (Flat Appl) in (let
697 TMP_435 \def (Bind Abst) in (let TMP_436 \def (THead TMP_435 u0 t2) in (let
698 TMP_437 \def (THead TMP_434 t0 TMP_436) in (let TMP_438 \def (Bind Abst) in
699 (let TMP_439 \def (THead TMP_438 x x2) in (pc3 c TMP_437 TMP_439))))))))) in
700 (let TMP_446 \def (\lambda (u0: T).(\lambda (t2: T).(let TMP_441 \def (Flat
701 Appl) in (let TMP_442 \def (TLRef x1) in (let TMP_443 \def (THeads TMP_441 t1
702 TMP_442) in (let TMP_444 \def (Bind Abst) in (let TMP_445 \def (THead TMP_444
703 u0 t2) in (ty3 g c TMP_443 TMP_445)))))))) in (let TMP_447 \def (\lambda (u0:
704 T).(\lambda (_: T).(ty3 g c t0 u0))) in (let TMP_455 \def (\lambda (v:
705 T).(\lambda (_: T).(let TMP_448 \def (Flat Appl) in (let TMP_449 \def (Flat
706 Appl) in (let TMP_450 \def (TLRef x1) in (let TMP_451 \def (THeads TMP_449 t1
707 TMP_450) in (let TMP_452 \def (THead TMP_448 t0 TMP_451) in (let TMP_453 \def
708 (Bind Abst) in (let TMP_454 \def (THead TMP_453 x v) in (eq T TMP_452
709 TMP_454)))))))))) in (let TMP_456 \def (\lambda (_: T).(\lambda (w0: T).(ty3
710 g c x w0))) in (let TMP_459 \def (\lambda (v: T).(\lambda (_: T).(let TMP_457
711 \def (Bind Abst) in (let TMP_458 \def (CHead c TMP_457 x) in (ty3 g TMP_458 v
712 x2))))) in (let TMP_462 \def (\lambda (v: T).(\lambda (_: T).(let TMP_460
713 \def (Bind Abst) in (let TMP_461 \def (CHead c TMP_460 x) in (nf2 TMP_461
714 v))))) in (let TMP_463 \def (ex4_2 T T TMP_455 TMP_456 TMP_459 TMP_462) in
715 (let TMP_557 \def (\lambda (x3: T).(\lambda (x4: T).(\lambda (H14: (pc3 c
716 (THead (Flat Appl) t0 (THead (Bind Abst) x3 x4)) (THead (Bind Abst) x
717 x2))).(\lambda (H15: (ty3 g c (THeads (Flat Appl) t1 (TLRef x1)) (THead (Bind
718 Abst) x3 x4))).(\lambda (_: (ty3 g c t0 x3)).(let H_y \def
719 (ty3_nf2_gen__ty3_nf2_inv_abst_aux c x x2 H13 t0 x3 x4 H14) in (let H_x0 \def
720 (H11 x3 x4 H15 H_y) in (let H17 \def H_x0 in (let TMP_469 \def (\lambda (v:
721 T).(\lambda (_: T).(let TMP_464 \def (Flat Appl) in (let TMP_465 \def (TLRef
722 x1) in (let TMP_466 \def (THeads TMP_464 t1 TMP_465) in (let TMP_467 \def
723 (Bind Abst) in (let TMP_468 \def (THead TMP_467 x3 v) in (eq T TMP_466
724 TMP_468)))))))) in (let TMP_470 \def (\lambda (_: T).(\lambda (w0: T).(ty3 g
725 c x3 w0))) in (let TMP_473 \def (\lambda (v: T).(\lambda (_: T).(let TMP_471
726 \def (Bind Abst) in (let TMP_472 \def (CHead c TMP_471 x3) in (ty3 g TMP_472
727 v x4))))) in (let TMP_476 \def (\lambda (v: T).(\lambda (_: T).(let TMP_474
728 \def (Bind Abst) in (let TMP_475 \def (CHead c TMP_474 x3) in (nf2 TMP_475
729 v))))) in (let TMP_484 \def (\lambda (v: T).(\lambda (_: T).(let TMP_477 \def
730 (Flat Appl) in (let TMP_478 \def (Flat Appl) in (let TMP_479 \def (TLRef x1)
731 in (let TMP_480 \def (THeads TMP_478 t1 TMP_479) in (let TMP_481 \def (THead
732 TMP_477 t0 TMP_480) in (let TMP_482 \def (Bind Abst) in (let TMP_483 \def
733 (THead TMP_482 x v) in (eq T TMP_481 TMP_483)))))))))) in (let TMP_485 \def
734 (\lambda (_: T).(\lambda (w0: T).(ty3 g c x w0))) in (let TMP_488 \def
735 (\lambda (v: T).(\lambda (_: T).(let TMP_486 \def (Bind Abst) in (let TMP_487
736 \def (CHead c TMP_486 x) in (ty3 g TMP_487 v x2))))) in (let TMP_491 \def
737 (\lambda (v: T).(\lambda (_: T).(let TMP_489 \def (Bind Abst) in (let TMP_490
738 \def (CHead c TMP_489 x) in (nf2 TMP_490 v))))) in (let TMP_492 \def (ex4_2 T
739 T TMP_484 TMP_485 TMP_488 TMP_491) in (let TMP_556 \def (\lambda (x5:
740 T).(\lambda (x6: T).(\lambda (H18: (eq T (THeads (Flat Appl) t1 (TLRef x1))
741 (THead (Bind Abst) x3 x5))).(\lambda (_: (ty3 g c x3 x6)).(\lambda (_: (ty3 g
742 (CHead c (Bind Abst) x3) x5 x4)).(\lambda (_: (nf2 (CHead c (Bind Abst) x3)
743 x5)).(let TMP_508 \def (\lambda (t2: TList).((eq T (THeads (Flat Appl) t2
744 (TLRef x1)) (THead (Bind Abst) x3 x5)) \to (let TMP_500 \def (\lambda (v:
745 T).(\lambda (_: T).(let TMP_493 \def (Flat Appl) in (let TMP_494 \def (Flat
746 Appl) in (let TMP_495 \def (TLRef x1) in (let TMP_496 \def (THeads TMP_494 t2
747 TMP_495) in (let TMP_497 \def (THead TMP_493 t0 TMP_496) in (let TMP_498 \def
748 (Bind Abst) in (let TMP_499 \def (THead TMP_498 x v) in (eq T TMP_497
749 TMP_499)))))))))) in (let TMP_501 \def (\lambda (_: T).(\lambda (w0: T).(ty3
750 g c x w0))) in (let TMP_504 \def (\lambda (v: T).(\lambda (_: T).(let TMP_502
751 \def (Bind Abst) in (let TMP_503 \def (CHead c TMP_502 x) in (ty3 g TMP_503 v
752 x2))))) in (let TMP_507 \def (\lambda (v: T).(\lambda (_: T).(let TMP_505
753 \def (Bind Abst) in (let TMP_506 \def (CHead c TMP_505 x) in (nf2 TMP_506
754 v))))) in (ex4_2 T T TMP_500 TMP_501 TMP_504 TMP_507))))))) in (let TMP_529
755 \def (\lambda (H22: (eq T (THeads (Flat Appl) TNil (TLRef x1)) (THead (Bind
756 Abst) x3 x5))).(let TMP_509 \def (TLRef x1) in (let TMP_510 \def (\lambda
757 (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow
758 True | (THead _ _ _) \Rightarrow False])) in (let TMP_511 \def (Bind Abst) in
759 (let TMP_512 \def (THead TMP_511 x3 x5) in (let H23 \def (eq_ind T TMP_509
760 TMP_510 I TMP_512 H22) in (let TMP_520 \def (\lambda (v: T).(\lambda (_:
761 T).(let TMP_513 \def (Flat Appl) in (let TMP_514 \def (Flat Appl) in (let
762 TMP_515 \def (TLRef x1) in (let TMP_516 \def (THeads TMP_514 TNil TMP_515) in
763 (let TMP_517 \def (THead TMP_513 t0 TMP_516) in (let TMP_518 \def (Bind Abst)
764 in (let TMP_519 \def (THead TMP_518 x v) in (eq T TMP_517 TMP_519))))))))))
765 in (let TMP_521 \def (\lambda (_: T).(\lambda (w0: T).(ty3 g c x w0))) in
766 (let TMP_524 \def (\lambda (v: T).(\lambda (_: T).(let TMP_522 \def (Bind
767 Abst) in (let TMP_523 \def (CHead c TMP_522 x) in (ty3 g TMP_523 v x2))))) in
768 (let TMP_527 \def (\lambda (v: T).(\lambda (_: T).(let TMP_525 \def (Bind
769 Abst) in (let TMP_526 \def (CHead c TMP_525 x) in (nf2 TMP_526 v))))) in (let
770 TMP_528 \def (ex4_2 T T TMP_520 TMP_521 TMP_524 TMP_527) in (False_ind
771 TMP_528 H23)))))))))))) in (let TMP_555 \def (\lambda (t2: T).(\lambda (t3:
772 TList).(\lambda (_: (((eq T (THeads (Flat Appl) t3 (TLRef x1)) (THead (Bind
773 Abst) x3 x5)) \to (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T (THead
774 (Flat Appl) t0 (THeads (Flat Appl) t3 (TLRef x1))) (THead (Bind Abst) x v))))
775 (\lambda (_: T).(\lambda (w0: T).(ty3 g c x w0))) (\lambda (v: T).(\lambda
776 (_: T).(ty3 g (CHead c (Bind Abst) x) v x2))) (\lambda (v: T).(\lambda (_:
777 T).(nf2 (CHead c (Bind Abst) x) v))))))).(\lambda (H22: (eq T (THeads (Flat
778 Appl) (TCons t2 t3) (TLRef x1)) (THead (Bind Abst) x3 x5))).(let TMP_530 \def
779 (Flat Appl) in (let TMP_531 \def (Flat Appl) in (let TMP_532 \def (TLRef x1)
780 in (let TMP_533 \def (THeads TMP_531 t3 TMP_532) in (let TMP_534 \def (THead
781 TMP_530 t2 TMP_533) in (let TMP_535 \def (\lambda (ee: T).(match ee with
782 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
783 \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
784 True])])) in (let TMP_536 \def (Bind Abst) in (let TMP_537 \def (THead
785 TMP_536 x3 x5) in (let H23 \def (eq_ind T TMP_534 TMP_535 I TMP_537 H22) in
786 (let TMP_546 \def (\lambda (v: T).(\lambda (_: T).(let TMP_538 \def (Flat
787 Appl) in (let TMP_539 \def (Flat Appl) in (let TMP_540 \def (TCons t2 t3) in
788 (let TMP_541 \def (TLRef x1) in (let TMP_542 \def (THeads TMP_539 TMP_540
789 TMP_541) in (let TMP_543 \def (THead TMP_538 t0 TMP_542) in (let TMP_544 \def
790 (Bind Abst) in (let TMP_545 \def (THead TMP_544 x v) in (eq T TMP_543
791 TMP_545))))))))))) in (let TMP_547 \def (\lambda (_: T).(\lambda (w0: T).(ty3
792 g c x w0))) in (let TMP_550 \def (\lambda (v: T).(\lambda (_: T).(let TMP_548
793 \def (Bind Abst) in (let TMP_549 \def (CHead c TMP_548 x) in (ty3 g TMP_549 v
794 x2))))) in (let TMP_553 \def (\lambda (v: T).(\lambda (_: T).(let TMP_551
795 \def (Bind Abst) in (let TMP_552 \def (CHead c TMP_551 x) in (nf2 TMP_552
796 v))))) in (let TMP_554 \def (ex4_2 T T TMP_546 TMP_547 TMP_550 TMP_553) in
797 (False_ind TMP_554 H23))))))))))))))))))) in (TList_ind TMP_508 TMP_529
798 TMP_555 t1 H18)))))))))) in (ex4_2_ind T T TMP_469 TMP_470 TMP_473 TMP_476
799 TMP_492 TMP_556 H17))))))))))))))))))) in (let TMP_558 \def (Flat Appl) in
800 (let TMP_559 \def (TLRef x1) in (let TMP_560 \def (THeads TMP_558 t1 TMP_559)
801 in (let TMP_561 \def (Bind Abst) in (let TMP_562 \def (THead TMP_561 x x2) in
802 (let TMP_563 \def (ty3_gen_appl g c t0 TMP_560 TMP_562 H12) in (ex3_2_ind T T
803 TMP_440 TMP_446 TMP_447 TMP_463 TMP_557 TMP_563))))))))))))))))))))))) in
804 (let TMP_565 \def (TList_ind TMP_327 TMP_433 TMP_564 x0) in (let TMP_566 \def
805 (unintro T w TMP_313 TMP_565) in (let TMP_567 \def (unintro T u TMP_299
806 TMP_566 H10) in (let TMP_568 \def (TMP_567 H9) in (eq_ind_r T TMP_274 TMP_285
807 TMP_568 t H5)))))))))))))))))))))))))) in (ex3_2_ind TList nat TMP_251
808 TMP_252 TMP_254 TMP_265 TMP_569 H4))))))))))) in (or3_ind TMP_10 TMP_13
809 TMP_21 TMP_32 TMP_199 TMP_247 TMP_570 H3))))))))))))))))))))))))))))))).
projects / helm.git / blob