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/props.ma".
20 \forall (x: T).(\forall (n: nat).((pr0 (TSort n) x) \to (eq T x (TSort n))))
22 \lambda (x: T).(\lambda (n: nat).(\lambda (H: (pr0 (TSort n) x)).(insert_eq
23 T (TSort n) (\lambda (t: T).(pr0 t x)) (\lambda (t: T).(eq T x t)) (\lambda
24 (y: T).(\lambda (H0: (pr0 y x)).(pr0_ind (\lambda (t: T).(\lambda (t0:
25 T).((eq T t (TSort n)) \to (eq T t0 t)))) (\lambda (t: T).(\lambda (H1: (eq T
26 t (TSort n))).(let H2 \def (f_equal T T (\lambda (e: T).e) t (TSort n) H1) in
27 (eq_ind_r T (TSort n) (\lambda (t0: T).(eq T t0 t0)) (refl_equal T (TSort n))
28 t H2)))) (\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda
29 (_: (((eq T u1 (TSort n)) \to (eq T u2 u1)))).(\lambda (t1: T).(\lambda (t2:
30 T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq T t2
31 t1)))).(\lambda (k: K).(\lambda (H5: (eq T (THead k u1 t1) (TSort n))).(let
32 H6 \def (eq_ind T (THead k u1 t1) (\lambda (ee: T).(match ee in T return
33 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
34 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H5) in
35 (False_ind (eq T (THead k u2 t2) (THead k u1 t1)) H6)))))))))))) (\lambda (u:
36 T).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_:
37 (((eq T v1 (TSort n)) \to (eq T v2 v1)))).(\lambda (t1: T).(\lambda (t2:
38 T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq T t2
39 t1)))).(\lambda (H5: (eq T (THead (Flat Appl) v1 (THead (Bind Abst) u t1))
40 (TSort n))).(let H6 \def (eq_ind T (THead (Flat Appl) v1 (THead (Bind Abst) u
41 t1)) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with
42 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
43 \Rightarrow True])) I (TSort n) H5) in (False_ind (eq T (THead (Bind Abbr) v2
44 t2) (THead (Flat Appl) v1 (THead (Bind Abst) u t1))) H6)))))))))))) (\lambda
45 (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2:
46 T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 (TSort n)) \to (eq T v2
47 v1)))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda
48 (_: (((eq T u1 (TSort n)) \to (eq T u2 u1)))).(\lambda (t1: T).(\lambda (t2:
49 T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq T t2
50 t1)))).(\lambda (H8: (eq T (THead (Flat Appl) v1 (THead (Bind b) u1 t1))
51 (TSort n))).(let H9 \def (eq_ind T (THead (Flat Appl) v1 (THead (Bind b) u1
52 t1)) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with
53 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
54 \Rightarrow True])) I (TSort n) H8) in (False_ind (eq T (THead (Bind b) u2
55 (THead (Flat Appl) (lift (S O) O v2) t2)) (THead (Flat Appl) v1 (THead (Bind
56 b) u1 t1))) H9))))))))))))))))) (\lambda (u1: T).(\lambda (u2: T).(\lambda
57 (_: (pr0 u1 u2)).(\lambda (_: (((eq T u1 (TSort n)) \to (eq T u2
58 u1)))).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (pr0 t1 t2)).(\lambda
59 (_: (((eq T t1 (TSort n)) \to (eq T t2 t1)))).(\lambda (w: T).(\lambda (_:
60 (subst0 O u2 t2 w)).(\lambda (H6: (eq T (THead (Bind Abbr) u1 t1) (TSort
61 n))).(let H7 \def (eq_ind T (THead (Bind Abbr) u1 t1) (\lambda (ee: T).(match
62 ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False |
63 (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n)
64 H6) in (False_ind (eq T (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u1 t1))
65 H7))))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda
66 (t1: T).(\lambda (t2: T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1
67 (TSort n)) \to (eq T t2 t1)))).(\lambda (u: T).(\lambda (H4: (eq T (THead
68 (Bind b) u (lift (S O) O t1)) (TSort n))).(let H5 \def (eq_ind T (THead (Bind
69 b) u (lift (S O) O t1)) (\lambda (ee: T).(match ee in T return (\lambda (_:
70 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
71 (THead _ _ _) \Rightarrow True])) I (TSort n) H4) in (False_ind (eq T t2
72 (THead (Bind b) u (lift (S O) O t1))) H5)))))))))) (\lambda (t1: T).(\lambda
73 (t2: T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq
74 T t2 t1)))).(\lambda (u: T).(\lambda (H3: (eq T (THead (Flat Cast) u t1)
75 (TSort n))).(let H4 \def (eq_ind T (THead (Flat Cast) u t1) (\lambda (ee:
76 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
77 False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I
78 (TSort n) H3) in (False_ind (eq T t2 (THead (Flat Cast) u t1)) H4)))))))) y x
85 \forall (x: T).(\forall (n: nat).((pr0 (TLRef n) x) \to (eq T x (TLRef n))))
87 \lambda (x: T).(\lambda (n: nat).(\lambda (H: (pr0 (TLRef n) x)).(insert_eq
88 T (TLRef n) (\lambda (t: T).(pr0 t x)) (\lambda (t: T).(eq T x t)) (\lambda
89 (y: T).(\lambda (H0: (pr0 y x)).(pr0_ind (\lambda (t: T).(\lambda (t0:
90 T).((eq T t (TLRef n)) \to (eq T t0 t)))) (\lambda (t: T).(\lambda (H1: (eq T
91 t (TLRef n))).(let H2 \def (f_equal T T (\lambda (e: T).e) t (TLRef n) H1) in
92 (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T t0 t0)) (refl_equal T (TLRef n))
93 t H2)))) (\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda
94 (_: (((eq T u1 (TLRef n)) \to (eq T u2 u1)))).(\lambda (t1: T).(\lambda (t2:
95 T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1 (TLRef n)) \to (eq T t2
96 t1)))).(\lambda (k: K).(\lambda (H5: (eq T (THead k u1 t1) (TLRef n))).(let
97 H6 \def (eq_ind T (THead k u1 t1) (\lambda (ee: T).(match ee in T return
98 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
99 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H5) in
100 (False_ind (eq T (THead k u2 t2) (THead k u1 t1)) H6)))))))))))) (\lambda (u:
101 T).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_:
102 (((eq T v1 (TLRef n)) \to (eq T v2 v1)))).(\lambda (t1: T).(\lambda (t2:
103 T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1 (TLRef n)) \to (eq T t2
104 t1)))).(\lambda (H5: (eq T (THead (Flat Appl) v1 (THead (Bind Abst) u t1))
105 (TLRef n))).(let H6 \def (eq_ind T (THead (Flat Appl) v1 (THead (Bind Abst) u
106 t1)) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with
107 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
108 \Rightarrow True])) I (TLRef n) H5) in (False_ind (eq T (THead (Bind Abbr) v2
109 t2) (THead (Flat Appl) v1 (THead (Bind Abst) u t1))) H6)))))))))))) (\lambda
110 (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2:
111 T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 (TLRef n)) \to (eq T v2
112 v1)))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda
113 (_: (((eq T u1 (TLRef n)) \to (eq T u2 u1)))).(\lambda (t1: T).(\lambda (t2:
114 T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1 (TLRef n)) \to (eq T t2
115 t1)))).(\lambda (H8: (eq T (THead (Flat Appl) v1 (THead (Bind b) u1 t1))
116 (TLRef n))).(let H9 \def (eq_ind T (THead (Flat Appl) v1 (THead (Bind b) u1
117 t1)) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with
118 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
119 \Rightarrow True])) I (TLRef n) H8) in (False_ind (eq T (THead (Bind b) u2
120 (THead (Flat Appl) (lift (S O) O v2) t2)) (THead (Flat Appl) v1 (THead (Bind
121 b) u1 t1))) H9))))))))))))))))) (\lambda (u1: T).(\lambda (u2: T).(\lambda
122 (_: (pr0 u1 u2)).(\lambda (_: (((eq T u1 (TLRef n)) \to (eq T u2
123 u1)))).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (pr0 t1 t2)).(\lambda
124 (_: (((eq T t1 (TLRef n)) \to (eq T t2 t1)))).(\lambda (w: T).(\lambda (_:
125 (subst0 O u2 t2 w)).(\lambda (H6: (eq T (THead (Bind Abbr) u1 t1) (TLRef
126 n))).(let H7 \def (eq_ind T (THead (Bind Abbr) u1 t1) (\lambda (ee: T).(match
127 ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False |
128 (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n)
129 H6) in (False_ind (eq T (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u1 t1))
130 H7))))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda
131 (t1: T).(\lambda (t2: T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1
132 (TLRef n)) \to (eq T t2 t1)))).(\lambda (u: T).(\lambda (H4: (eq T (THead
133 (Bind b) u (lift (S O) O t1)) (TLRef n))).(let H5 \def (eq_ind T (THead (Bind
134 b) u (lift (S O) O t1)) (\lambda (ee: T).(match ee in T return (\lambda (_:
135 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
136 (THead _ _ _) \Rightarrow True])) I (TLRef n) H4) in (False_ind (eq T t2
137 (THead (Bind b) u (lift (S O) O t1))) H5)))))))))) (\lambda (t1: T).(\lambda
138 (t2: T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1 (TLRef n)) \to (eq
139 T t2 t1)))).(\lambda (u: T).(\lambda (H3: (eq T (THead (Flat Cast) u t1)
140 (TLRef n))).(let H4 \def (eq_ind T (THead (Flat Cast) u t1) (\lambda (ee:
141 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
142 False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I
143 (TLRef n) H3) in (False_ind (eq T t2 (THead (Flat Cast) u t1)) H4)))))))) y x
149 theorem pr0_gen_abst:
150 \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Bind Abst) u1
151 t1) x) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Bind
152 Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
153 T).(\lambda (t2: T).(pr0 t1 t2)))))))
155 \lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (H: (pr0 (THead
156 (Bind Abst) u1 t1) x)).(insert_eq T (THead (Bind Abst) u1 t1) (\lambda (t:
157 T).(pr0 t x)) (\lambda (_: T).(ex3_2 T T (\lambda (u2: T).(\lambda (t2:
158 T).(eq T x (THead (Bind Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0
159 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2))))) (\lambda (y:
160 T).(\lambda (H0: (pr0 y x)).(pr0_ind (\lambda (t: T).(\lambda (t0: T).((eq T
161 t (THead (Bind Abst) u1 t1)) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
162 T).(eq T t0 (THead (Bind Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_:
163 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2))))))) (\lambda
164 (t: T).(\lambda (H1: (eq T t (THead (Bind Abst) u1 t1))).(let H2 \def
165 (f_equal T T (\lambda (e: T).e) t (THead (Bind Abst) u1 t1) H1) in (eq_ind_r
166 T (THead (Bind Abst) u1 t1) (\lambda (t0: T).(ex3_2 T T (\lambda (u2:
167 T).(\lambda (t2: T).(eq T t0 (THead (Bind Abst) u2 t2)))) (\lambda (u2:
168 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1
169 t2))))) (ex3_2_intro T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Bind
170 Abst) u1 t1) (THead (Bind Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_:
171 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2))) u1 t1
172 (refl_equal T (THead (Bind Abst) u1 t1)) (pr0_refl u1) (pr0_refl t1)) t
173 H2)))) (\lambda (u0: T).(\lambda (u2: T).(\lambda (H1: (pr0 u0 u2)).(\lambda
174 (H2: (((eq T u0 (THead (Bind Abst) u1 t1)) \to (ex3_2 T T (\lambda (u3:
175 T).(\lambda (t2: T).(eq T u2 (THead (Bind Abst) u3 t2)))) (\lambda (u3:
176 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1
177 t2))))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H3: (pr0 t0
178 t2)).(\lambda (H4: (((eq T t0 (THead (Bind Abst) u1 t1)) \to (ex3_2 T T
179 (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst) u3 t3))))
180 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
181 T).(pr0 t1 t3))))))).(\lambda (k: K).(\lambda (H5: (eq T (THead k u0 t0)
182 (THead (Bind Abst) u1 t1))).(let H6 \def (f_equal T K (\lambda (e: T).(match
183 e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _)
184 \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k u0 t0) (THead (Bind
185 Abst) u1 t1) H5) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e in T
186 return (\lambda (_: T).T) with [(TSort _) \Rightarrow u0 | (TLRef _)
187 \Rightarrow u0 | (THead _ t _) \Rightarrow t])) (THead k u0 t0) (THead (Bind
188 Abst) u1 t1) H5) in ((let H8 \def (f_equal T T (\lambda (e: T).(match e in T
189 return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _)
190 \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead k u0 t0) (THead (Bind
191 Abst) u1 t1) H5) in (\lambda (H9: (eq T u0 u1)).(\lambda (H10: (eq K k (Bind
192 Abst))).(eq_ind_r K (Bind Abst) (\lambda (k0: K).(ex3_2 T T (\lambda (u3:
193 T).(\lambda (t3: T).(eq T (THead k0 u2 t2) (THead (Bind Abst) u3 t3))))
194 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
195 T).(pr0 t1 t3))))) (let H11 \def (eq_ind T t0 (\lambda (t: T).((eq T t (THead
196 (Bind Abst) u1 t1)) \to (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2
197 (THead (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3)))
198 (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))))) H4 t1 H8) in (let H12 \def
199 (eq_ind T t0 (\lambda (t: T).(pr0 t t2)) H3 t1 H8) in (let H13 \def (eq_ind T
200 u0 (\lambda (t: T).((eq T t (THead (Bind Abst) u1 t1)) \to (ex3_2 T T
201 (\lambda (u3: T).(\lambda (t3: T).(eq T u2 (THead (Bind Abst) u3 t3))))
202 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
203 T).(pr0 t1 t3)))))) H2 u1 H9) in (let H14 \def (eq_ind T u0 (\lambda (t:
204 T).(pr0 t u2)) H1 u1 H9) in (ex3_2_intro T T (\lambda (u3: T).(\lambda (t3:
205 T).(eq T (THead (Bind Abst) u2 t2) (THead (Bind Abst) u3 t3)))) (\lambda (u3:
206 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
207 t3))) u2 t2 (refl_equal T (THead (Bind Abst) u2 t2)) H14 H12))))) k H10))))
208 H7)) H6)))))))))))) (\lambda (u: T).(\lambda (v1: T).(\lambda (v2:
209 T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind Abst) u1
210 t1)) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Bind
211 Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
212 T).(\lambda (t2: T).(pr0 t1 t2))))))).(\lambda (t0: T).(\lambda (t2:
213 T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind Abst) u1
214 t1)) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
215 Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
216 T).(\lambda (t3: T).(pr0 t1 t3))))))).(\lambda (H5: (eq T (THead (Flat Appl)
217 v1 (THead (Bind Abst) u t0)) (THead (Bind Abst) u1 t1))).(let H6 \def (eq_ind
218 T (THead (Flat Appl) v1 (THead (Bind Abst) u t0)) (\lambda (ee: T).(match ee
219 in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef
220 _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return
221 (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
222 True])])) I (THead (Bind Abst) u1 t1) H5) in (False_ind (ex3_2 T T (\lambda
223 (u2: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abst)
224 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
225 T).(\lambda (t3: T).(pr0 t1 t3)))) H6)))))))))))) (\lambda (b: B).(\lambda
226 (_: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0
227 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind Abst) u1 t1)) \to (ex3_2 T T
228 (\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Bind Abst) u2 t2))))
229 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2:
230 T).(pr0 t1 t2))))))).(\lambda (u0: T).(\lambda (u2: T).(\lambda (_: (pr0 u0
231 u2)).(\lambda (_: (((eq T u0 (THead (Bind Abst) u1 t1)) \to (ex3_2 T T
232 (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead (Bind Abst) u3 t2))))
233 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t2:
234 T).(pr0 t1 t2))))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0
235 t2)).(\lambda (_: (((eq T t0 (THead (Bind Abst) u1 t1)) \to (ex3_2 T T
236 (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst) u3 t3))))
237 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
238 T).(pr0 t1 t3))))))).(\lambda (H8: (eq T (THead (Flat Appl) v1 (THead (Bind
239 b) u0 t0)) (THead (Bind Abst) u1 t1))).(let H9 \def (eq_ind T (THead (Flat
240 Appl) v1 (THead (Bind b) u0 t0)) (\lambda (ee: T).(match ee in T return
241 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
242 \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda
243 (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
244 True])])) I (THead (Bind Abst) u1 t1) H8) in (False_ind (ex3_2 T T (\lambda
245 (u3: T).(\lambda (t3: T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S
246 O) O v2) t2)) (THead (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_:
247 T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3))))
248 H9))))))))))))))))) (\lambda (u0: T).(\lambda (u2: T).(\lambda (_: (pr0 u0
249 u2)).(\lambda (_: (((eq T u0 (THead (Bind Abst) u1 t1)) \to (ex3_2 T T
250 (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead (Bind Abst) u3 t2))))
251 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t2:
252 T).(pr0 t1 t2))))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0
253 t2)).(\lambda (_: (((eq T t0 (THead (Bind Abst) u1 t1)) \to (ex3_2 T T
254 (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst) u3 t3))))
255 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
256 T).(pr0 t1 t3))))))).(\lambda (w: T).(\lambda (_: (subst0 O u2 t2
257 w)).(\lambda (H6: (eq T (THead (Bind Abbr) u0 t0) (THead (Bind Abst) u1
258 t1))).(let H7 \def (eq_ind T (THead (Bind Abbr) u0 t0) (\lambda (ee:
259 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
260 False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K
261 return (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return
262 (\lambda (_: B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False |
263 Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (THead (Bind
264 Abst) u1 t1) H6) in (False_ind (ex3_2 T T (\lambda (u3: T).(\lambda (t3:
265 T).(eq T (THead (Bind Abbr) u2 w) (THead (Bind Abst) u3 t3)))) (\lambda (u3:
266 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
267 t3)))) H7))))))))))))) (\lambda (b: B).(\lambda (H1: (not (eq B b
268 Abst))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda
269 (H3: (((eq T t0 (THead (Bind Abst) u1 t1)) \to (ex3_2 T T (\lambda (u2:
270 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst) u2 t3)))) (\lambda (u2:
271 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
272 t3))))))).(\lambda (u: T).(\lambda (H4: (eq T (THead (Bind b) u (lift (S O) O
273 t0)) (THead (Bind Abst) u1 t1))).(let H5 \def (f_equal T B (\lambda (e:
274 T).(match e in T return (\lambda (_: T).B) with [(TSort _) \Rightarrow b |
275 (TLRef _) \Rightarrow b | (THead k _ _) \Rightarrow (match k in K return
276 (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow
277 b])])) (THead (Bind b) u (lift (S O) O t0)) (THead (Bind Abst) u1 t1) H4) in
278 ((let H6 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_:
279 T).T) with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t _)
280 \Rightarrow t])) (THead (Bind b) u (lift (S O) O t0)) (THead (Bind Abst) u1
281 t1) H4) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e in T return
282 (\lambda (_: T).T) with [(TSort _) \Rightarrow ((let rec lref_map (f: ((nat
283 \to nat))) (d: nat) (t: T) on t: T \def (match t with [(TSort n) \Rightarrow
284 (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with [true
285 \Rightarrow i | false \Rightarrow (f i)])) | (THead k u0 t3) \Rightarrow
286 (THead k (lref_map f d u0) (lref_map f (s k d) t3))]) in lref_map) (\lambda
287 (x0: nat).(plus x0 (S O))) O t0) | (TLRef _) \Rightarrow ((let rec lref_map
288 (f: ((nat \to nat))) (d: nat) (t: T) on t: T \def (match t with [(TSort n)
289 \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with
290 [true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u0 t3)
291 \Rightarrow (THead k (lref_map f d u0) (lref_map f (s k d) t3))]) in
292 lref_map) (\lambda (x0: nat).(plus x0 (S O))) O t0) | (THead _ _ t)
293 \Rightarrow t])) (THead (Bind b) u (lift (S O) O t0)) (THead (Bind Abst) u1
294 t1) H4) in (\lambda (_: (eq T u u1)).(\lambda (H9: (eq B b Abst)).(let H10
295 \def (eq_ind B b (\lambda (b0: B).(not (eq B b0 Abst))) H1 Abst H9) in (let
296 H11 \def (eq_ind_r T t1 (\lambda (t: T).((eq T t0 (THead (Bind Abst) u1 t))
297 \to (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst)
298 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
299 T).(\lambda (t3: T).(pr0 t t3)))))) H3 (lift (S O) O t0) H7) in (eq_ind T
300 (lift (S O) O t0) (\lambda (t: T).(ex3_2 T T (\lambda (u2: T).(\lambda (t3:
301 T).(eq T t2 (THead (Bind Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_:
302 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t t3))))) (let H12
303 \def (match (H10 (refl_equal B Abst)) in False return (\lambda (_:
304 False).(ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
305 Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
306 T).(\lambda (t3: T).(pr0 (lift (S O) O t0) t3))))) with []) in H12) t1
307 H7)))))) H6)) H5)))))))))) (\lambda (t0: T).(\lambda (t2: T).(\lambda (_:
308 (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind Abst) u1 t1)) \to (ex3_2 T
309 T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst) u2 t3))))
310 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
311 T).(pr0 t1 t3))))))).(\lambda (u: T).(\lambda (H3: (eq T (THead (Flat Cast) u
312 t0) (THead (Bind Abst) u1 t1))).(let H4 \def (eq_ind T (THead (Flat Cast) u
313 t0) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
314 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
315 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
316 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind Abst) u1
317 t1) H3) in (False_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2
318 (THead (Bind Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))
319 (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) H4)))))))) y x H0))) H)))).
324 theorem pr0_gen_appl:
325 \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Flat Appl) u1
326 t1) x) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead
327 (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
328 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1:
329 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
330 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
331 (t2: T).(eq T x (THead (Bind Abbr) u2 t2)))))) (\lambda (_: T).(\lambda (_:
332 T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
333 (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))) (ex6_6 B T T T T T
334 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
335 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
336 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
337 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
338 T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t2: T).(eq T x (THead (Bind b)
339 v2 (THead (Flat Appl) (lift (S O) O u2) t2))))))))) (\lambda (_: B).(\lambda
340 (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0
341 u1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
342 T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_:
343 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
344 (t2: T).(pr0 z1 t2))))))))))))
346 \lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (H: (pr0 (THead
347 (Flat Appl) u1 t1) x)).(insert_eq T (THead (Flat Appl) u1 t1) (\lambda (t:
348 T).(pr0 t x)) (\lambda (_: T).(or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
349 T).(eq T x (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0
350 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T
351 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
352 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
353 T).(\lambda (t2: T).(eq T x (THead (Bind Abbr) u2 t2)))))) (\lambda (_:
354 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda
355 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2))))))
356 (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
357 (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
358 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
359 (_: T).(eq T t1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
360 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t2: T).(eq T x
361 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2))))))))) (\lambda
362 (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
363 T).(\lambda (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda (y1:
364 T).(\lambda (_: T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1
365 v2))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_:
366 T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))))))) (\lambda (y:
367 T).(\lambda (H0: (pr0 y x)).(pr0_ind (\lambda (t: T).(\lambda (t0: T).((eq T
368 t (THead (Flat Appl) u1 t1)) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda
369 (t2: T).(eq T t0 (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_:
370 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T
371 T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
372 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
373 T).(\lambda (t2: T).(eq T t0 (THead (Bind Abbr) u2 t2)))))) (\lambda (_:
374 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda
375 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2))))))
376 (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
377 (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
378 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
379 (_: T).(eq T t1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
380 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t2: T).(eq T
381 t0 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2)))))))))
382 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
383 T).(\lambda (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda (y1:
384 T).(\lambda (_: T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1
385 v2))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_:
386 T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))))))))) (\lambda (t:
387 T).(\lambda (H1: (eq T t (THead (Flat Appl) u1 t1))).(let H2 \def (f_equal T
388 T (\lambda (e: T).e) t (THead (Flat Appl) u1 t1) H1) in (eq_ind_r T (THead
389 (Flat Appl) u1 t1) (\lambda (t0: T).(or3 (ex3_2 T T (\lambda (u2: T).(\lambda
390 (t2: T).(eq T t0 (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_:
391 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T
392 T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
393 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
394 T).(\lambda (t2: T).(eq T t0 (THead (Bind Abbr) u2 t2)))))) (\lambda (_:
395 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda
396 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2))))))
397 (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
398 (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
399 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
400 (_: T).(eq T t1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
401 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t2: T).(eq T
402 t0 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2)))))))))
403 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
404 T).(\lambda (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda (y1:
405 T).(\lambda (_: T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1
406 v2))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_:
407 T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))))))) (or3_intro0 (ex3_2 T
408 T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Flat Appl) u1 t1) (THead
409 (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
410 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1:
411 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
412 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
413 (t2: T).(eq T (THead (Flat Appl) u1 t1) (THead (Bind Abbr) u2 t2))))))
414 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1
415 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2:
416 T).(pr0 z1 t2)))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_:
417 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
418 b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
419 T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind b) y1 z1))))))))
420 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
421 (v2: T).(\lambda (t2: T).(eq T (THead (Flat Appl) u1 t1) (THead (Bind b) v2
422 (THead (Flat Appl) (lift (S O) O u2) t2))))))))) (\lambda (_: B).(\lambda (_:
423 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
424 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
425 T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_:
426 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
427 (t2: T).(pr0 z1 t2)))))))) (ex3_2_intro T T (\lambda (u2: T).(\lambda (t2:
428 T).(eq T (THead (Flat Appl) u1 t1) (THead (Flat Appl) u2 t2)))) (\lambda (u2:
429 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1
430 t2))) u1 t1 (refl_equal T (THead (Flat Appl) u1 t1)) (pr0_refl u1) (pr0_refl
431 t1))) t H2)))) (\lambda (u0: T).(\lambda (u2: T).(\lambda (H1: (pr0 u0
432 u2)).(\lambda (H2: (((eq T u0 (THead (Flat Appl) u1 t1)) \to (or3 (ex3_2 T T
433 (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead (Flat Appl) u3 t2))))
434 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t2:
435 T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
436 (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
437 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead (Bind
438 Abbr) u3 t2)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
439 (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
440 T).(\lambda (t2: T).(pr0 z1 t2)))))) (ex6_6 B T T T T T (\lambda (b:
441 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
442 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
443 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
444 b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
445 (u3: T).(\lambda (v2: T).(\lambda (t2: T).(eq T u2 (THead (Bind b) v2 (THead
446 (Flat Appl) (lift (S O) O u3) t2))))))))) (\lambda (_: B).(\lambda (_:
447 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
448 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
449 T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_:
450 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
451 (t2: T).(pr0 z1 t2)))))))))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda
452 (H3: (pr0 t0 t2)).(\lambda (H4: (((eq T t0 (THead (Flat Appl) u1 t1)) \to
453 (or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl)
454 u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
455 T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
456 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1
457 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3:
458 T).(eq T t2 (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_:
459 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
460 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
461 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
462 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
463 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
464 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
465 T).(\lambda (u3: T).(\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
466 b) v2 (THead (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_:
467 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
468 (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
469 T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2)))))))
470 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
471 T).(\lambda (t3: T).(pr0 z1 t3)))))))))))).(\lambda (k: K).(\lambda (H5: (eq
472 T (THead k u0 t0) (THead (Flat Appl) u1 t1))).(let H6 \def (f_equal T K
473 (\lambda (e: T).(match e in T return (\lambda (_: T).K) with [(TSort _)
474 \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _) \Rightarrow k0]))
475 (THead k u0 t0) (THead (Flat Appl) u1 t1) H5) in ((let H7 \def (f_equal T T
476 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
477 \Rightarrow u0 | (TLRef _) \Rightarrow u0 | (THead _ t _) \Rightarrow t]))
478 (THead k u0 t0) (THead (Flat Appl) u1 t1) H5) in ((let H8 \def (f_equal T T
479 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
480 \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) \Rightarrow t]))
481 (THead k u0 t0) (THead (Flat Appl) u1 t1) H5) in (\lambda (H9: (eq T u0
482 u1)).(\lambda (H10: (eq K k (Flat Appl))).(eq_ind_r K (Flat Appl) (\lambda
483 (k0: K).(or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead k0 u2
484 t2) (THead (Flat Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1
485 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda
486 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead
487 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3:
488 T).(\lambda (t3: T).(eq T (THead k0 u2 t2) (THead (Bind Abbr) u3 t3))))))
489 (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1
490 u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3:
491 T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_:
492 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
493 b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
494 T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind b) y1 z1))))))))
495 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
496 (v2: T).(\lambda (t3: T).(eq T (THead k0 u2 t2) (THead (Bind b) v2 (THead
497 (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_: B).(\lambda (_:
498 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
499 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
500 T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_:
501 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
502 (t3: T).(pr0 z1 t3)))))))))) (let H11 \def (eq_ind T t0 (\lambda (t: T).((eq
503 T t (THead (Flat Appl) u1 t1)) \to (or3 (ex3_2 T T (\lambda (u3: T).(\lambda
504 (t3: T).(eq T t2 (THead (Flat Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_:
505 T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T
506 T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
507 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3:
508 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u3 t3)))))) (\lambda (_:
509 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda
510 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3))))))
511 (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
512 (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
513 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
514 (_: T).(eq T t1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
515 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (v2: T).(\lambda (t3: T).(eq T
516 t2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3) t3)))))))))
517 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_:
518 T).(\lambda (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1:
519 T).(\lambda (_: T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1
520 v2))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_:
521 T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3))))))))))) H4 t1 H8) in (let
522 H12 \def (eq_ind T t0 (\lambda (t: T).(pr0 t t2)) H3 t1 H8) in (let H13 \def
523 (eq_ind T u0 (\lambda (t: T).((eq T t (THead (Flat Appl) u1 t1)) \to (or3
524 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T u2 (THead (Flat Appl) u3
525 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
526 T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
527 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1
528 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3:
529 T).(eq T u2 (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_:
530 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
531 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
532 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
533 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
534 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
535 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
536 T).(\lambda (u3: T).(\lambda (v2: T).(\lambda (t3: T).(eq T u2 (THead (Bind
537 b) v2 (THead (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_:
538 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
539 (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
540 T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2)))))))
541 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
542 T).(\lambda (t3: T).(pr0 z1 t3))))))))))) H2 u1 H9) in (let H14 \def (eq_ind
543 T u0 (\lambda (t: T).(pr0 t u2)) H1 u1 H9) in (or3_intro0 (ex3_2 T T (\lambda
544 (u3: T).(\lambda (t3: T).(eq T (THead (Flat Appl) u2 t2) (THead (Flat Appl)
545 u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
546 T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
547 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1
548 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3:
549 T).(eq T (THead (Flat Appl) u2 t2) (THead (Bind Abbr) u3 t3)))))) (\lambda
550 (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3)))))
551 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1
552 t3)))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_:
553 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst))))))))
554 (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
555 (_: T).(\lambda (_: T).(eq T t1 (THead (Bind b) y1 z1)))))))) (\lambda (b:
556 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (v2: T).(\lambda
557 (t3: T).(eq T (THead (Flat Appl) u2 t2) (THead (Bind b) v2 (THead (Flat Appl)
558 (lift (S O) O u3) t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_:
559 T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u3)))))))
560 (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
561 (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_: B).(\lambda (_:
562 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1
563 t3)))))))) (ex3_2_intro T T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead
564 (Flat Appl) u2 t2) (THead (Flat Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_:
565 T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3))) u2 t2
566 (refl_equal T (THead (Flat Appl) u2 t2)) H14 H12)))))) k H10)))) H7))
567 H6)))))))))))) (\lambda (u: T).(\lambda (v1: T).(\lambda (v2: T).(\lambda
568 (H1: (pr0 v1 v2)).(\lambda (H2: (((eq T v1 (THead (Flat Appl) u1 t1)) \to
569 (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Flat Appl)
570 u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
571 T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
572 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1
573 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t2:
574 T).(eq T v2 (THead (Bind Abbr) u2 t2)))))) (\lambda (_: T).(\lambda (_:
575 T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
576 (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))) (ex6_6 B T T T T T
577 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
578 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
579 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
580 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
581 T).(\lambda (u2: T).(\lambda (v3: T).(\lambda (t2: T).(eq T v2 (THead (Bind
582 b) v3 (THead (Flat Appl) (lift (S O) O u2) t2))))))))) (\lambda (_:
583 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda
584 (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
585 T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3)))))))
586 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
587 T).(\lambda (t2: T).(pr0 z1 t2)))))))))))).(\lambda (t0: T).(\lambda (t2:
588 T).(\lambda (H3: (pr0 t0 t2)).(\lambda (H4: (((eq T t0 (THead (Flat Appl) u1
589 t1)) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead
590 (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
591 (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1:
592 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
593 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
594 (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
595 T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
596 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
597 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
598 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
599 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
600 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
601 T).(\lambda (u2: T).(\lambda (v3: T).(\lambda (t3: T).(eq T t2 (THead (Bind
602 b) v3 (THead (Flat Appl) (lift (S O) O u2) t3))))))))) (\lambda (_:
603 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda
604 (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
605 T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3)))))))
606 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
607 T).(\lambda (t3: T).(pr0 z1 t3)))))))))))).(\lambda (H5: (eq T (THead (Flat
608 Appl) v1 (THead (Bind Abst) u t0)) (THead (Flat Appl) u1 t1))).(let H6 \def
609 (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with
610 [(TSort _) \Rightarrow v1 | (TLRef _) \Rightarrow v1 | (THead _ t _)
611 \Rightarrow t])) (THead (Flat Appl) v1 (THead (Bind Abst) u t0)) (THead (Flat
612 Appl) u1 t1) H5) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e in T
613 return (\lambda (_: T).T) with [(TSort _) \Rightarrow (THead (Bind Abst) u
614 t0) | (TLRef _) \Rightarrow (THead (Bind Abst) u t0) | (THead _ _ t)
615 \Rightarrow t])) (THead (Flat Appl) v1 (THead (Bind Abst) u t0)) (THead (Flat
616 Appl) u1 t1) H5) in (\lambda (H8: (eq T v1 u1)).(let H9 \def (eq_ind T v1
617 (\lambda (t: T).((eq T t (THead (Flat Appl) u1 t1)) \to (or3 (ex3_2 T T
618 (\lambda (u2: T).(\lambda (t3: T).(eq T v2 (THead (Flat Appl) u2 t3))))
619 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
620 T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
621 (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
622 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T v2 (THead (Bind
623 Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
624 (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
625 T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b:
626 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
627 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
628 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
629 b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
630 (u2: T).(\lambda (v3: T).(\lambda (t3: T).(eq T v2 (THead (Bind b) v3 (THead
631 (Flat Appl) (lift (S O) O u2) t3))))))))) (\lambda (_: B).(\lambda (_:
632 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
633 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
634 T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_:
635 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
636 (t3: T).(pr0 z1 t3))))))))))) H2 u1 H8) in (let H10 \def (eq_ind T v1
637 (\lambda (t: T).(pr0 t v2)) H1 u1 H8) in (let H11 \def (eq_ind_r T t1
638 (\lambda (t: T).((eq T t0 (THead (Flat Appl) u1 t)) \to (or3 (ex3_2 T T
639 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3))))
640 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
641 T).(pr0 t t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
642 (_: T).(\lambda (_: T).(eq T t (THead (Bind Abst) y1 z1)))))) (\lambda (_:
643 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
644 Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
645 (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
646 T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b:
647 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
648 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
649 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t (THead (Bind
650 b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
651 (u2: T).(\lambda (v3: T).(\lambda (t3: T).(eq T t2 (THead (Bind b) v3 (THead
652 (Flat Appl) (lift (S O) O u2) t3))))))))) (\lambda (_: B).(\lambda (_:
653 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
654 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
655 T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_:
656 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
657 (t3: T).(pr0 z1 t3))))))))))) H4 (THead (Bind Abst) u t0) H7) in (let H12
658 \def (eq_ind_r T t1 (\lambda (t: T).((eq T u1 (THead (Flat Appl) u1 t)) \to
659 (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T v2 (THead (Flat Appl)
660 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
661 T).(\lambda (t3: T).(pr0 t t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
662 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t (THead (Bind Abst) y1
663 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3:
664 T).(eq T v2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
665 T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
666 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
667 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
668 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
669 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t
670 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
671 T).(\lambda (u2: T).(\lambda (v3: T).(\lambda (t3: T).(eq T v2 (THead (Bind
672 b) v3 (THead (Flat Appl) (lift (S O) O u2) t3))))))))) (\lambda (_:
673 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda
674 (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
675 T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3)))))))
676 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
677 T).(\lambda (t3: T).(pr0 z1 t3))))))))))) H9 (THead (Bind Abst) u t0) H7) in
678 (eq_ind T (THead (Bind Abst) u t0) (\lambda (t: T).(or3 (ex3_2 T T (\lambda
679 (u2: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) v2 t2) (THead (Flat Appl)
680 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
681 T).(\lambda (t3: T).(pr0 t t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
682 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t (THead (Bind Abst) y1
683 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3:
684 T).(eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abbr) u2 t3)))))) (\lambda
685 (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))))
686 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1
687 t3)))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_:
688 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst))))))))
689 (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
690 (_: T).(\lambda (_: T).(eq T t (THead (Bind b) y1 z1)))))))) (\lambda (b:
691 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (v3: T).(\lambda
692 (t3: T).(eq T (THead (Bind Abbr) v2 t2) (THead (Bind b) v3 (THead (Flat Appl)
693 (lift (S O) O u2) t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_:
694 T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u2)))))))
695 (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
696 (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_: B).(\lambda (_:
697 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1
698 t3)))))))))) (or3_intro1 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T
699 (THead (Bind Abbr) v2 t2) (THead (Flat Appl) u2 t3)))) (\lambda (u2:
700 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 (THead
701 (Bind Abst) u t0) t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1:
702 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind Abst) u t0) (THead
703 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
704 T).(\lambda (t3: T).(eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abbr) u2
705 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
706 T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
707 (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_:
708 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
709 b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
710 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind Abst) u t0) (THead
711 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
712 T).(\lambda (u2: T).(\lambda (v3: T).(\lambda (t3: T).(eq T (THead (Bind
713 Abbr) v2 t2) (THead (Bind b) v3 (THead (Flat Appl) (lift (S O) O u2)
714 t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
715 T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda
716 (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0
717 y1 v3))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_:
718 T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))))) (ex4_4_intro T T T T
719 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
720 (THead (Bind Abst) u t0) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
721 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T (THead (Bind Abbr)
722 v2 t2) (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
723 T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
724 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3))))) u t0 v2 t2
725 (refl_equal T (THead (Bind Abst) u t0)) (refl_equal T (THead (Bind Abbr) v2
726 t2)) H10 H3)) t1 H7))))))) H6)))))))))))) (\lambda (b: B).(\lambda (H1: (not
727 (eq B b Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (H2: (pr0 v1
728 v2)).(\lambda (H3: (((eq T v1 (THead (Flat Appl) u1 t1)) \to (or3 (ex3_2 T T
729 (\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Flat Appl) u2 t2))))
730 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2:
731 T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
732 (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
733 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Bind
734 Abbr) u2 t2)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
735 (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
736 T).(\lambda (t2: T).(pr0 z1 t2)))))) (ex6_6 B T T T T T (\lambda (b0:
737 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
738 (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda
739 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
740 b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda
741 (u2: T).(\lambda (v3: T).(\lambda (t2: T).(eq T v2 (THead (Bind b0) v3 (THead
742 (Flat Appl) (lift (S O) O u2) t2))))))))) (\lambda (_: B).(\lambda (_:
743 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
744 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
745 T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_:
746 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
747 (t2: T).(pr0 z1 t2)))))))))))).(\lambda (u0: T).(\lambda (u2: T).(\lambda
748 (H4: (pr0 u0 u2)).(\lambda (H5: (((eq T u0 (THead (Flat Appl) u1 t1)) \to
749 (or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead (Flat Appl)
750 u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
751 T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
752 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1
753 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t2:
754 T).(eq T u2 (THead (Bind Abbr) u3 t2)))))) (\lambda (_: T).(\lambda (_:
755 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
756 (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))) (ex6_6 B T T T T T
757 (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
758 T).(\lambda (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1:
759 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
760 (THead (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
761 T).(\lambda (u3: T).(\lambda (v3: T).(\lambda (t2: T).(eq T u2 (THead (Bind
762 b0) v3 (THead (Flat Appl) (lift (S O) O u3) t2))))))))) (\lambda (_:
763 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
764 (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
765 T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3)))))))
766 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
767 T).(\lambda (t2: T).(pr0 z1 t2)))))))))))).(\lambda (t0: T).(\lambda (t2:
768 T).(\lambda (H6: (pr0 t0 t2)).(\lambda (H7: (((eq T t0 (THead (Flat Appl) u1
769 t1)) \to (or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead
770 (Flat Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
771 (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1:
772 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
773 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
774 (t3: T).(eq T t2 (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_:
775 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
776 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
777 (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
778 T).(\lambda (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1:
779 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
780 (THead (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
781 T).(\lambda (u3: T).(\lambda (v3: T).(\lambda (t3: T).(eq T t2 (THead (Bind
782 b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_:
783 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
784 (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
785 T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3)))))))
786 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
787 T).(\lambda (t3: T).(pr0 z1 t3)))))))))))).(\lambda (H8: (eq T (THead (Flat
788 Appl) v1 (THead (Bind b) u0 t0)) (THead (Flat Appl) u1 t1))).(let H9 \def
789 (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with
790 [(TSort _) \Rightarrow v1 | (TLRef _) \Rightarrow v1 | (THead _ t _)
791 \Rightarrow t])) (THead (Flat Appl) v1 (THead (Bind b) u0 t0)) (THead (Flat
792 Appl) u1 t1) H8) in ((let H10 \def (f_equal T T (\lambda (e: T).(match e in T
793 return (\lambda (_: T).T) with [(TSort _) \Rightarrow (THead (Bind b) u0 t0)
794 | (TLRef _) \Rightarrow (THead (Bind b) u0 t0) | (THead _ _ t) \Rightarrow
795 t])) (THead (Flat Appl) v1 (THead (Bind b) u0 t0)) (THead (Flat Appl) u1 t1)
796 H8) in (\lambda (H11: (eq T v1 u1)).(let H12 \def (eq_ind T v1 (\lambda (t:
797 T).((eq T t (THead (Flat Appl) u1 t1)) \to (or3 (ex3_2 T T (\lambda (u3:
798 T).(\lambda (t3: T).(eq T v2 (THead (Flat Appl) u3 t3)))) (\lambda (u3:
799 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
800 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
801 T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
802 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3: T).(eq T v2 (THead (Bind
803 Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
804 (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
805 T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b0:
806 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
807 (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda
808 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
809 b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda
810 (u3: T).(\lambda (v3: T).(\lambda (t3: T).(eq T v2 (THead (Bind b0) v3 (THead
811 (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_: B).(\lambda (_:
812 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
813 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
814 T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_:
815 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
816 (t3: T).(pr0 z1 t3))))))))))) H3 u1 H11) in (let H13 \def (eq_ind T v1
817 (\lambda (t: T).(pr0 t v2)) H2 u1 H11) in (let H14 \def (eq_ind_r T t1
818 (\lambda (t: T).((eq T t0 (THead (Flat Appl) u1 t)) \to (or3 (ex3_2 T T
819 (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u3 t3))))
820 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
821 T).(pr0 t t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
822 (_: T).(\lambda (_: T).(eq T t (THead (Bind Abst) y1 z1)))))) (\lambda (_:
823 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind
824 Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
825 (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
826 T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b0:
827 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
828 (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda
829 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t (THead (Bind
830 b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda
831 (u3: T).(\lambda (v3: T).(\lambda (t3: T).(eq T t2 (THead (Bind b0) v3 (THead
832 (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_: B).(\lambda (_:
833 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
834 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
835 T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_:
836 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
837 (t3: T).(pr0 z1 t3))))))))))) H7 (THead (Bind b) u0 t0) H10) in (let H15 \def
838 (eq_ind_r T t1 (\lambda (t: T).((eq T u0 (THead (Flat Appl) u1 t)) \to (or3
839 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T u2 (THead (Flat Appl) u3
840 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
841 T).(\lambda (t3: T).(pr0 t t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
842 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t (THead (Bind Abst) y1
843 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3:
844 T).(eq T u2 (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_:
845 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
846 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
847 (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
848 T).(\lambda (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1:
849 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t
850 (THead (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
851 T).(\lambda (u3: T).(\lambda (v3: T).(\lambda (t3: T).(eq T u2 (THead (Bind
852 b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_:
853 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
854 (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
855 T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3)))))))
856 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
857 T).(\lambda (t3: T).(pr0 z1 t3))))))))))) H5 (THead (Bind b) u0 t0) H10) in
858 (let H16 \def (eq_ind_r T t1 (\lambda (t: T).((eq T u1 (THead (Flat Appl) u1
859 t)) \to (or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T v2 (THead
860 (Flat Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
861 (_: T).(\lambda (t3: T).(pr0 t t3)))) (ex4_4 T T T T (\lambda (y1:
862 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t (THead (Bind
863 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
864 (t3: T).(eq T v2 (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_:
865 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
866 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
867 (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
868 T).(\lambda (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1:
869 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t
870 (THead (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
871 T).(\lambda (u3: T).(\lambda (v3: T).(\lambda (t3: T).(eq T v2 (THead (Bind
872 b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_:
873 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
874 (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
875 T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3)))))))
876 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
877 T).(\lambda (t3: T).(pr0 z1 t3))))))))))) H12 (THead (Bind b) u0 t0) H10) in
878 (eq_ind T (THead (Bind b) u0 t0) (\lambda (t: T).(or3 (ex3_2 T T (\lambda
879 (u3: T).(\lambda (t3: T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S
880 O) O v2) t2)) (THead (Flat Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_:
881 T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t t3)))) (ex4_4 T T T
882 T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t
883 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3:
884 T).(\lambda (t3: T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O
885 v2) t2)) (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_:
886 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
887 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
888 (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
889 T).(\lambda (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1:
890 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t
891 (THead (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
892 T).(\lambda (u3: T).(\lambda (v3: T).(\lambda (t3: T).(eq T (THead (Bind b)
893 u2 (THead (Flat Appl) (lift (S O) O v2) t2)) (THead (Bind b0) v3 (THead (Flat
894 Appl) (lift (S O) O u3) t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda
895 (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u3)))))))
896 (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
897 (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_: B).(\lambda (_:
898 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1
899 t3)))))))))) (or3_intro2 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T
900 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)) (THead (Flat
901 Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
902 T).(\lambda (t3: T).(pr0 (THead (Bind b) u0 t0) t3)))) (ex4_4 T T T T
903 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
904 (THead (Bind b) u0 t0) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
905 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind b) u2
906 (THead (Flat Appl) (lift (S O) O v2) t2)) (THead (Bind Abbr) u3 t3))))))
907 (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1
908 u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3:
909 T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b0: B).(\lambda (_:
910 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
911 b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda
912 (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind b) u0 t0) (THead
913 (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
914 T).(\lambda (u3: T).(\lambda (v3: T).(\lambda (t3: T).(eq T (THead (Bind b)
915 u2 (THead (Flat Appl) (lift (S O) O v2) t2)) (THead (Bind b0) v3 (THead (Flat
916 Appl) (lift (S O) O u3) t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda
917 (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u3)))))))
918 (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
919 (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_: B).(\lambda (_:
920 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1
921 t3)))))))) (ex6_6_intro B T T T T T (\lambda (b0: B).(\lambda (_: T).(\lambda
922 (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b0
923 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
924 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind b) u0 t0) (THead (Bind
925 b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda
926 (u3: T).(\lambda (v3: T).(\lambda (t3: T).(eq T (THead (Bind b) u2 (THead
927 (Flat Appl) (lift (S O) O v2) t2)) (THead (Bind b0) v3 (THead (Flat Appl)
928 (lift (S O) O u3) t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_:
929 T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u3)))))))
930 (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
931 (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_: B).(\lambda (_:
932 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1
933 t3))))))) b u0 t0 v2 u2 t2 H1 (refl_equal T (THead (Bind b) u0 t0))
934 (refl_equal T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)))
935 H13 H4 H6)) t1 H10)))))))) H9))))))))))))))))) (\lambda (u0: T).(\lambda (u2:
936 T).(\lambda (_: (pr0 u0 u2)).(\lambda (_: (((eq T u0 (THead (Flat Appl) u1
937 t1)) \to (or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead
938 (Flat Appl) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
939 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1:
940 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
941 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
942 (t2: T).(eq T u2 (THead (Bind Abbr) u3 t2)))))) (\lambda (_: T).(\lambda (_:
943 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
944 (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))) (ex6_6 B T T T T T
945 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
946 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
947 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
948 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
949 T).(\lambda (u3: T).(\lambda (v2: T).(\lambda (t2: T).(eq T u2 (THead (Bind
950 b) v2 (THead (Flat Appl) (lift (S O) O u3) t2))))))))) (\lambda (_:
951 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
952 (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
953 T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2)))))))
954 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
955 T).(\lambda (t2: T).(pr0 z1 t2)))))))))))).(\lambda (t0: T).(\lambda (t2:
956 T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Flat Appl) u1
957 t1)) \to (or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead
958 (Flat Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
959 (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1:
960 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
961 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
962 (t3: T).(eq T t2 (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_:
963 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
964 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
965 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
966 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
967 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
968 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
969 T).(\lambda (u3: T).(\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
970 b) v2 (THead (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_:
971 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
972 (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
973 T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2)))))))
974 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
975 T).(\lambda (t3: T).(pr0 z1 t3)))))))))))).(\lambda (w: T).(\lambda (_:
976 (subst0 O u2 t2 w)).(\lambda (H6: (eq T (THead (Bind Abbr) u0 t0) (THead
977 (Flat Appl) u1 t1))).(let H7 \def (eq_ind T (THead (Bind Abbr) u0 t0)
978 (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
979 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
980 (match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True |
981 (Flat _) \Rightarrow False])])) I (THead (Flat Appl) u1 t1) H6) in (False_ind
982 (or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) u2
983 w) (THead (Flat Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1
984 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda
985 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead
986 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3:
987 T).(\lambda (t3: T).(eq T (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u3
988 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_:
989 T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
990 (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_:
991 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
992 b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
993 T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind b) y1 z1))))))))
994 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
995 (v2: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) u2 w) (THead (Bind b) v2
996 (THead (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_: B).(\lambda (_:
997 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
998 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
999 T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_:
1000 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1001 (t3: T).(pr0 z1 t3))))))))) H7))))))))))))) (\lambda (b: B).(\lambda (_: (not
1002 (eq B b Abst))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0
1003 t2)).(\lambda (_: (((eq T t0 (THead (Flat Appl) u1 t1)) \to (or3 (ex3_2 T T
1004 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3))))
1005 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
1006 T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
1007 (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
1008 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
1009 Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1010 (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
1011 T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b0:
1012 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1013 (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda
1014 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
1015 b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda
1016 (u2: T).(\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind b0) v2 (THead
1017 (Flat Appl) (lift (S O) O u2) t3))))))))) (\lambda (_: B).(\lambda (_:
1018 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
1019 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
1020 T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_:
1021 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1022 (t3: T).(pr0 z1 t3)))))))))))).(\lambda (u: T).(\lambda (H4: (eq T (THead
1023 (Bind b) u (lift (S O) O t0)) (THead (Flat Appl) u1 t1))).(let H5 \def
1024 (eq_ind T (THead (Bind b) u (lift (S O) O t0)) (\lambda (ee: T).(match ee in
1025 T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
1026 \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda
1027 (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow
1028 False])])) I (THead (Flat Appl) u1 t1) H4) in (False_ind (or3 (ex3_2 T T
1029 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3))))
1030 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
1031 T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
1032 (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
1033 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
1034 Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1035 (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
1036 T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b0:
1037 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1038 (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda
1039 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
1040 b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda
1041 (u2: T).(\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind b0) v2 (THead
1042 (Flat Appl) (lift (S O) O u2) t3))))))))) (\lambda (_: B).(\lambda (_:
1043 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
1044 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
1045 T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_:
1046 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1047 (t3: T).(pr0 z1 t3))))))))) H5)))))))))) (\lambda (t0: T).(\lambda (t2:
1048 T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Flat Appl) u1
1049 t1)) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead
1050 (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
1051 (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1:
1052 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
1053 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1054 (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
1055 T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
1056 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
1057 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1058 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
1059 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
1060 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
1061 T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
1062 b) v2 (THead (Flat Appl) (lift (S O) O u2) t3))))))))) (\lambda (_:
1063 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda
1064 (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1065 T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2)))))))
1066 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
1067 T).(\lambda (t3: T).(pr0 z1 t3)))))))))))).(\lambda (u: T).(\lambda (H3: (eq
1068 T (THead (Flat Cast) u t0) (THead (Flat Appl) u1 t1))).(let H4 \def (eq_ind T
1069 (THead (Flat Cast) u t0) (\lambda (ee: T).(match ee in T return (\lambda (_:
1070 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
1071 (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with
1072 [(Bind _) \Rightarrow False | (Flat f) \Rightarrow (match f in F return
1073 (\lambda (_: F).Prop) with [Appl \Rightarrow False | Cast \Rightarrow
1074 True])])])) I (THead (Flat Appl) u1 t1) H3) in (False_ind (or3 (ex3_2 T T
1075 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3))))
1076 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
1077 T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
1078 (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
1079 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
1080 Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1081 (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
1082 T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b:
1083 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1084 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
1085 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
1086 b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
1087 (u2: T).(\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind b) v2 (THead
1088 (Flat Appl) (lift (S O) O u2) t3))))))))) (\lambda (_: B).(\lambda (_:
1089 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
1090 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
1091 T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_:
1092 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1093 (t3: T).(pr0 z1 t3))))))))) H4)))))))) y x H0))) H)))).
1095 Initial nodes: 12299
1098 theorem pr0_gen_cast:
1099 \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Flat Cast) u1
1100 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead
1101 (Flat Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
1102 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 x)))))
1104 \lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (H: (pr0 (THead
1105 (Flat Cast) u1 t1) x)).(insert_eq T (THead (Flat Cast) u1 t1) (\lambda (t:
1106 T).(pr0 t x)) (\lambda (_: T).(or (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
1107 T).(eq T x (THead (Flat Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0
1108 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 x)))
1109 (\lambda (y: T).(\lambda (H0: (pr0 y x)).(pr0_ind (\lambda (t: T).(\lambda
1110 (t0: T).((eq T t (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u2:
1111 T).(\lambda (t2: T).(eq T t0 (THead (Flat Cast) u2 t2)))) (\lambda (u2:
1112 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1
1113 t2)))) (pr0 t1 t0))))) (\lambda (t: T).(\lambda (H1: (eq T t (THead (Flat
1114 Cast) u1 t1))).(let H2 \def (f_equal T T (\lambda (e: T).e) t (THead (Flat
1115 Cast) u1 t1) H1) in (eq_ind_r T (THead (Flat Cast) u1 t1) (\lambda (t0:
1116 T).(or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead (Flat
1117 Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
1118 T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 t0))) (or_introl (ex3_2 T T
1119 (\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Flat Cast) u1 t1) (THead
1120 (Flat Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
1121 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 (THead (Flat Cast) u1 t1))
1122 (ex3_2_intro T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Flat Cast)
1123 u1 t1) (THead (Flat Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1
1124 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2))) u1 t1 (refl_equal T
1125 (THead (Flat Cast) u1 t1)) (pr0_refl u1) (pr0_refl t1))) t H2)))) (\lambda
1126 (u0: T).(\lambda (u2: T).(\lambda (H1: (pr0 u0 u2)).(\lambda (H2: (((eq T u0
1127 (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2:
1128 T).(eq T u2 (THead (Flat Cast) u3 t2)))) (\lambda (u3: T).(\lambda (_:
1129 T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1
1130 u2))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H3: (pr0 t0 t2)).(\lambda
1131 (H4: (((eq T t0 (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u3:
1132 T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u3 t3)))) (\lambda (u3:
1133 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
1134 t3)))) (pr0 t1 t2))))).(\lambda (k: K).(\lambda (H5: (eq T (THead k u0 t0)
1135 (THead (Flat Cast) u1 t1))).(let H6 \def (f_equal T K (\lambda (e: T).(match
1136 e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _)
1137 \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k u0 t0) (THead (Flat
1138 Cast) u1 t1) H5) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e in T
1139 return (\lambda (_: T).T) with [(TSort _) \Rightarrow u0 | (TLRef _)
1140 \Rightarrow u0 | (THead _ t _) \Rightarrow t])) (THead k u0 t0) (THead (Flat
1141 Cast) u1 t1) H5) in ((let H8 \def (f_equal T T (\lambda (e: T).(match e in T
1142 return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _)
1143 \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead k u0 t0) (THead (Flat
1144 Cast) u1 t1) H5) in (\lambda (H9: (eq T u0 u1)).(\lambda (H10: (eq K k (Flat
1145 Cast))).(eq_ind_r K (Flat Cast) (\lambda (k0: K).(or (ex3_2 T T (\lambda (u3:
1146 T).(\lambda (t3: T).(eq T (THead k0 u2 t2) (THead (Flat Cast) u3 t3))))
1147 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
1148 T).(pr0 t1 t3)))) (pr0 t1 (THead k0 u2 t2)))) (let H11 \def (eq_ind T t0
1149 (\lambda (t: T).((eq T t (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T
1150 (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u3 t3))))
1151 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
1152 T).(pr0 t1 t3)))) (pr0 t1 t2)))) H4 t1 H8) in (let H12 \def (eq_ind T t0
1153 (\lambda (t: T).(pr0 t t2)) H3 t1 H8) in (let H13 \def (eq_ind T u0 (\lambda
1154 (t: T).((eq T t (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u3:
1155 T).(\lambda (t3: T).(eq T u2 (THead (Flat Cast) u3 t3)))) (\lambda (u3:
1156 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
1157 t3)))) (pr0 t1 u2)))) H2 u1 H9) in (let H14 \def (eq_ind T u0 (\lambda (t:
1158 T).(pr0 t u2)) H1 u1 H9) in (or_introl (ex3_2 T T (\lambda (u3: T).(\lambda
1159 (t3: T).(eq T (THead (Flat Cast) u2 t2) (THead (Flat Cast) u3 t3)))) (\lambda
1160 (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0
1161 t1 t3)))) (pr0 t1 (THead (Flat Cast) u2 t2)) (ex3_2_intro T T (\lambda (u3:
1162 T).(\lambda (t3: T).(eq T (THead (Flat Cast) u2 t2) (THead (Flat Cast) u3
1163 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
1164 T).(\lambda (t3: T).(pr0 t1 t3))) u2 t2 (refl_equal T (THead (Flat Cast) u2
1165 t2)) H14 H12)))))) k H10)))) H7)) H6)))))))))))) (\lambda (u: T).(\lambda
1166 (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1
1167 (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
1168 T).(eq T v2 (THead (Flat Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_:
1169 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1
1170 v2))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda
1171 (_: (((eq T t0 (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u2:
1172 T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u2 t3)))) (\lambda (u2:
1173 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
1174 t3)))) (pr0 t1 t2))))).(\lambda (H5: (eq T (THead (Flat Appl) v1 (THead (Bind
1175 Abst) u t0)) (THead (Flat Cast) u1 t1))).(let H6 \def (eq_ind T (THead (Flat
1176 Appl) v1 (THead (Bind Abst) u t0)) (\lambda (ee: T).(match ee in T return
1177 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
1178 \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda
1179 (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow (match f
1180 in F return (\lambda (_: F).Prop) with [Appl \Rightarrow True | Cast
1181 \Rightarrow False])])])) I (THead (Flat Cast) u1 t1) H5) in (False_ind (or
1182 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) v2 t2)
1183 (THead (Flat Cast) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))
1184 (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (THead (Bind Abbr) v2
1185 t2))) H6)))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b
1186 Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda
1187 (_: (((eq T v1 (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u2:
1188 T).(\lambda (t2: T).(eq T v2 (THead (Flat Cast) u2 t2)))) (\lambda (u2:
1189 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1
1190 t2)))) (pr0 t1 v2))))).(\lambda (u0: T).(\lambda (u2: T).(\lambda (_: (pr0 u0
1191 u2)).(\lambda (_: (((eq T u0 (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T
1192 (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead (Flat Cast) u3 t2))))
1193 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t2:
1194 T).(pr0 t1 t2)))) (pr0 t1 u2))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda
1195 (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Flat Cast) u1 t1)) \to (or
1196 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u3
1197 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
1198 T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 t2))))).(\lambda (H8: (eq T (THead
1199 (Flat Appl) v1 (THead (Bind b) u0 t0)) (THead (Flat Cast) u1 t1))).(let H9
1200 \def (eq_ind T (THead (Flat Appl) v1 (THead (Bind b) u0 t0)) (\lambda (ee:
1201 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
1202 False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K
1203 return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat f)
1204 \Rightarrow (match f in F return (\lambda (_: F).Prop) with [Appl \Rightarrow
1205 True | Cast \Rightarrow False])])])) I (THead (Flat Cast) u1 t1) H8) in
1206 (False_ind (or (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead
1207 (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)) (THead (Flat Cast) u3
1208 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
1209 T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (THead (Bind b) u2 (THead (Flat
1210 Appl) (lift (S O) O v2) t2)))) H9))))))))))))))))) (\lambda (u0: T).(\lambda
1211 (u2: T).(\lambda (_: (pr0 u0 u2)).(\lambda (_: (((eq T u0 (THead (Flat Cast)
1212 u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead
1213 (Flat Cast) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
1214 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 u2))))).(\lambda (t0:
1215 T).(\lambda (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead
1216 (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq
1217 T t2 (THead (Flat Cast) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1
1218 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1
1219 t2))))).(\lambda (w: T).(\lambda (_: (subst0 O u2 t2 w)).(\lambda (H6: (eq T
1220 (THead (Bind Abbr) u0 t0) (THead (Flat Cast) u1 t1))).(let H7 \def (eq_ind T
1221 (THead (Bind Abbr) u0 t0) (\lambda (ee: T).(match ee in T return (\lambda (_:
1222 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
1223 (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with
1224 [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat
1225 Cast) u1 t1) H6) in (False_ind (or (ex3_2 T T (\lambda (u3: T).(\lambda (t3:
1226 T).(eq T (THead (Bind Abbr) u2 w) (THead (Flat Cast) u3 t3)))) (\lambda (u3:
1227 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
1228 t3)))) (pr0 t1 (THead (Bind Abbr) u2 w))) H7))))))))))))) (\lambda (b:
1229 B).(\lambda (_: (not (eq B b Abst))).(\lambda (t0: T).(\lambda (t2:
1230 T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Flat Cast) u1
1231 t1)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead
1232 (Flat Cast) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
1233 (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 t2))))).(\lambda (u:
1234 T).(\lambda (H4: (eq T (THead (Bind b) u (lift (S O) O t0)) (THead (Flat
1235 Cast) u1 t1))).(let H5 \def (eq_ind T (THead (Bind b) u (lift (S O) O t0))
1236 (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
1237 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
1238 (match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True |
1239 (Flat _) \Rightarrow False])])) I (THead (Flat Cast) u1 t1) H4) in (False_ind
1240 (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast)
1241 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
1242 T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 t2)) H5)))))))))) (\lambda (t0:
1243 T).(\lambda (t2: T).(\lambda (H1: (pr0 t0 t2)).(\lambda (H2: (((eq T t0
1244 (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3:
1245 T).(eq T t2 (THead (Flat Cast) u2 t3)))) (\lambda (u2: T).(\lambda (_:
1246 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1
1247 t2))))).(\lambda (u: T).(\lambda (H3: (eq T (THead (Flat Cast) u t0) (THead
1248 (Flat Cast) u1 t1))).(let H4 \def (f_equal T T (\lambda (e: T).(match e in T
1249 return (\lambda (_: T).T) with [(TSort _) \Rightarrow u | (TLRef _)
1250 \Rightarrow u | (THead _ t _) \Rightarrow t])) (THead (Flat Cast) u t0)
1251 (THead (Flat Cast) u1 t1) H3) in ((let H5 \def (f_equal T T (\lambda (e:
1252 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 |
1253 (TLRef _) \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead (Flat Cast)
1254 u t0) (THead (Flat Cast) u1 t1) H3) in (\lambda (_: (eq T u u1)).(let H7 \def
1255 (eq_ind T t0 (\lambda (t: T).((eq T t (THead (Flat Cast) u1 t1)) \to (or
1256 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u2
1257 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
1258 T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 t2)))) H2 t1 H5) in (let H8 \def
1259 (eq_ind T t0 (\lambda (t: T).(pr0 t t2)) H1 t1 H5) in (or_intror (ex3_2 T T
1260 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u2 t3))))
1261 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
1262 T).(pr0 t1 t3)))) (pr0 t1 t2) H8))))) H4)))))))) y x H0))) H)))).
1267 theorem pr0_gen_abbr:
1268 \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Bind Abbr) u1
1269 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead
1270 (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
1271 (u2: T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T (\lambda (y: T).(pr0 t1 y))
1272 (\lambda (y: T).(subst0 O u2 y t2))))))) (pr0 t1 (lift (S O) O x))))))
1274 \lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (H: (pr0 (THead
1275 (Bind Abbr) u1 t1) x)).(insert_eq T (THead (Bind Abbr) u1 t1) (\lambda (t:
1276 T).(pr0 t x)) (\lambda (_: T).(or (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
1277 T).(eq T x (THead (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0
1278 u1 u2))) (\lambda (u2: T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T (\lambda
1279 (y: T).(pr0 t1 y)) (\lambda (y: T).(subst0 O u2 y t2))))))) (pr0 t1 (lift (S
1280 O) O x)))) (\lambda (y: T).(\lambda (H0: (pr0 y x)).(pr0_ind (\lambda (t:
1281 T).(\lambda (t0: T).((eq T t (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T
1282 (\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead (Bind Abbr) u2 t2))))
1283 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: T).(\lambda (t2:
1284 T).(or (pr0 t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0:
1285 T).(subst0 O u2 y0 t2))))))) (pr0 t1 (lift (S O) O t0)))))) (\lambda (t:
1286 T).(\lambda (H1: (eq T t (THead (Bind Abbr) u1 t1))).(let H2 \def (f_equal T
1287 T (\lambda (e: T).e) t (THead (Bind Abbr) u1 t1) H1) in (eq_ind_r T (THead
1288 (Bind Abbr) u1 t1) (\lambda (t0: T).(or (ex3_2 T T (\lambda (u2: T).(\lambda
1289 (t2: T).(eq T t0 (THead (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_:
1290 T).(pr0 u1 u2))) (\lambda (u2: T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T
1291 (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u2 y0 t2))))))) (pr0
1292 t1 (lift (S O) O t0)))) (or_introl (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
1293 T).(eq T (THead (Bind Abbr) u1 t1) (THead (Bind Abbr) u2 t2)))) (\lambda (u2:
1294 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: T).(\lambda (t2: T).(or (pr0
1295 t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u2 y0
1296 t2))))))) (pr0 t1 (lift (S O) O (THead (Bind Abbr) u1 t1))) (ex3_2_intro T T
1297 (\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Bind Abbr) u1 t1) (THead
1298 (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
1299 (u2: T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
1300 (\lambda (y0: T).(subst0 O u2 y0 t2)))))) u1 t1 (refl_equal T (THead (Bind
1301 Abbr) u1 t1)) (pr0_refl u1) (or_introl (pr0 t1 t1) (ex2 T (\lambda (y0:
1302 T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u1 y0 t1))) (pr0_refl t1)))) t
1303 H2)))) (\lambda (u0: T).(\lambda (u2: T).(\lambda (H1: (pr0 u0 u2)).(\lambda
1304 (H2: (((eq T u0 (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u3:
1305 T).(\lambda (t2: T).(eq T u2 (THead (Bind Abbr) u3 t2)))) (\lambda (u3:
1306 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t2: T).(or (pr0
1307 t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u3 y0
1308 t2))))))) (pr0 t1 (lift (S O) O u2)))))).(\lambda (t0: T).(\lambda (t2:
1309 T).(\lambda (H3: (pr0 t0 t2)).(\lambda (H4: (((eq T t0 (THead (Bind Abbr) u1
1310 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead
1311 (Bind Abbr) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
1312 (u3: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
1313 (\lambda (y0: T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O
1314 t2)))))).(\lambda (k: K).(\lambda (H5: (eq T (THead k u0 t0) (THead (Bind
1315 Abbr) u1 t1))).(let H6 \def (f_equal T K (\lambda (e: T).(match e in T return
1316 (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k |
1317 (THead k0 _ _) \Rightarrow k0])) (THead k u0 t0) (THead (Bind Abbr) u1 t1)
1318 H5) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e in T return
1319 (\lambda (_: T).T) with [(TSort _) \Rightarrow u0 | (TLRef _) \Rightarrow u0
1320 | (THead _ t _) \Rightarrow t])) (THead k u0 t0) (THead (Bind Abbr) u1 t1)
1321 H5) in ((let H8 \def (f_equal T T (\lambda (e: T).(match e in T return
1322 (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0
1323 | (THead _ _ t) \Rightarrow t])) (THead k u0 t0) (THead (Bind Abbr) u1 t1)
1324 H5) in (\lambda (H9: (eq T u0 u1)).(\lambda (H10: (eq K k (Bind
1325 Abbr))).(eq_ind_r K (Bind Abbr) (\lambda (k0: K).(or (ex3_2 T T (\lambda (u3:
1326 T).(\lambda (t3: T).(eq T (THead k0 u2 t2) (THead (Bind Abbr) u3 t3))))
1327 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t3:
1328 T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0:
1329 T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O (THead k0 u2 t2))))) (let
1330 H11 \def (eq_ind T t0 (\lambda (t: T).((eq T t (THead (Bind Abbr) u1 t1)) \to
1331 (or (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr)
1332 u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3:
1333 T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
1334 (\lambda (y0: T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O t2))))) H4
1335 t1 H8) in (let H12 \def (eq_ind T t0 (\lambda (t: T).(pr0 t t2)) H3 t1 H8) in
1336 (let H13 \def (eq_ind T u0 (\lambda (t: T).((eq T t (THead (Bind Abbr) u1
1337 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T u2 (THead
1338 (Bind Abbr) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
1339 (u3: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
1340 (\lambda (y0: T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O u2))))) H2
1341 u1 H9) in (let H14 \def (eq_ind T u0 (\lambda (t: T).(pr0 t u2)) H1 u1 H9) in
1342 (or_introl (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind
1343 Abbr) u2 t2) (THead (Bind Abbr) u3 t3)))) (\lambda (u3: T).(\lambda (_:
1344 T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T
1345 (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u3 y0 t3))))))) (pr0
1346 t1 (lift (S O) O (THead (Bind Abbr) u2 t2))) (ex3_2_intro T T (\lambda (u3:
1347 T).(\lambda (t3: T).(eq T (THead (Bind Abbr) u2 t2) (THead (Bind Abbr) u3
1348 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3:
1349 T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
1350 (\lambda (y0: T).(subst0 O u3 y0 t3)))))) u2 t2 (refl_equal T (THead (Bind
1351 Abbr) u2 t2)) H14 (or_introl (pr0 t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
1352 (\lambda (y0: T).(subst0 O u2 y0 t2))) H12))))))) k H10)))) H7))
1353 H6)))))))))))) (\lambda (u: T).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_:
1354 (pr0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind Abbr) u1 t1)) \to (or
1355 (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Bind Abbr) u2
1356 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2:
1357 T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
1358 (\lambda (y0: T).(subst0 O u2 y0 t2))))))) (pr0 t1 (lift (S O) O
1359 v2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda
1360 (_: (((eq T t0 (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u2:
1361 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))) (\lambda (u2:
1362 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: T).(\lambda (t3: T).(or (pr0
1363 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u2 y0
1364 t3))))))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (H5: (eq T (THead (Flat
1365 Appl) v1 (THead (Bind Abst) u t0)) (THead (Bind Abbr) u1 t1))).(let H6 \def
1366 (eq_ind T (THead (Flat Appl) v1 (THead (Bind Abst) u t0)) (\lambda (ee:
1367 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
1368 False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K
1369 return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _)
1370 \Rightarrow True])])) I (THead (Bind Abbr) u1 t1) H5) in (False_ind (or
1371 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) v2 t2)
1372 (THead (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))
1373 (\lambda (u2: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0:
1374 T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t1 (lift (S
1375 O) O (THead (Bind Abbr) v2 t2)))) H6)))))))))))) (\lambda (b: B).(\lambda (_:
1376 (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1
1377 v2)).(\lambda (_: (((eq T v1 (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T
1378 (\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Bind Abbr) u2 t2))))
1379 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: T).(\lambda (t2:
1380 T).(or (pr0 t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0:
1381 T).(subst0 O u2 y0 t2))))))) (pr0 t1 (lift (S O) O v2)))))).(\lambda (u0:
1382 T).(\lambda (u2: T).(\lambda (_: (pr0 u0 u2)).(\lambda (_: (((eq T u0 (THead
1383 (Bind Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq
1384 T u2 (THead (Bind Abbr) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1
1385 u3))) (\lambda (u3: T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T (\lambda (y0:
1386 T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u3 y0 t2))))))) (pr0 t1 (lift (S
1387 O) O u2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0
1388 t2)).(\lambda (_: (((eq T t0 (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T
1389 (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u3 t3))))
1390 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t3:
1391 T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0:
1392 T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (H8: (eq
1393 T (THead (Flat Appl) v1 (THead (Bind b) u0 t0)) (THead (Bind Abbr) u1
1394 t1))).(let H9 \def (eq_ind T (THead (Flat Appl) v1 (THead (Bind b) u0 t0))
1395 (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
1396 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
1397 (match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False |
1398 (Flat _) \Rightarrow True])])) I (THead (Bind Abbr) u1 t1) H8) in (False_ind
1399 (or (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind b) u2
1400 (THead (Flat Appl) (lift (S O) O v2) t2)) (THead (Bind Abbr) u3 t3))))
1401 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t3:
1402 T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0:
1403 T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O (THead (Bind b) u2 (THead
1404 (Flat Appl) (lift (S O) O v2) t2))))) H9))))))))))))))))) (\lambda (u0:
1405 T).(\lambda (u2: T).(\lambda (H1: (pr0 u0 u2)).(\lambda (H2: (((eq T u0
1406 (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2:
1407 T).(eq T u2 (THead (Bind Abbr) u3 t2)))) (\lambda (u3: T).(\lambda (_:
1408 T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T
1409 (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u3 y0 t2))))))) (pr0
1410 t1 (lift (S O) O u2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H3:
1411 (pr0 t0 t2)).(\lambda (H4: (((eq T t0 (THead (Bind Abbr) u1 t1)) \to (or
1412 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u3
1413 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3:
1414 T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
1415 (\lambda (y0: T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O
1416 t2)))))).(\lambda (w: T).(\lambda (H5: (subst0 O u2 t2 w)).(\lambda (H6: (eq
1417 T (THead (Bind Abbr) u0 t0) (THead (Bind Abbr) u1 t1))).(let H7 \def (f_equal
1418 T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
1419 \Rightarrow u0 | (TLRef _) \Rightarrow u0 | (THead _ t _) \Rightarrow t]))
1420 (THead (Bind Abbr) u0 t0) (THead (Bind Abbr) u1 t1) H6) in ((let H8 \def
1421 (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with
1422 [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t)
1423 \Rightarrow t])) (THead (Bind Abbr) u0 t0) (THead (Bind Abbr) u1 t1) H6) in
1424 (\lambda (H9: (eq T u0 u1)).(let H10 \def (eq_ind T t0 (\lambda (t: T).((eq T
1425 t (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda
1426 (t3: T).(eq T t2 (THead (Bind Abbr) u3 t3)))) (\lambda (u3: T).(\lambda (_:
1427 T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T
1428 (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u3 y0 t3))))))) (pr0
1429 t1 (lift (S O) O t2))))) H4 t1 H8) in (let H11 \def (eq_ind T t0 (\lambda (t:
1430 T).(pr0 t t2)) H3 t1 H8) in (let H12 \def (eq_ind T u0 (\lambda (t: T).((eq T
1431 t (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda
1432 (t3: T).(eq T u2 (THead (Bind Abbr) u3 t3)))) (\lambda (u3: T).(\lambda (_:
1433 T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T
1434 (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u3 y0 t3))))))) (pr0
1435 t1 (lift (S O) O u2))))) H2 u1 H9) in (let H13 \def (eq_ind T u0 (\lambda (t:
1436 T).(pr0 t u2)) H1 u1 H9) in (or_introl (ex3_2 T T (\lambda (u3: T).(\lambda
1437 (t3: T).(eq T (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u3 t3)))) (\lambda
1438 (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t3: T).(or
1439 (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O
1440 u3 y0 t3))))))) (pr0 t1 (lift (S O) O (THead (Bind Abbr) u2 w))) (ex3_2_intro
1441 T T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) u2 w) (THead
1442 (Bind Abbr) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
1443 (u3: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
1444 (\lambda (y0: T).(subst0 O u3 y0 t3)))))) u2 w (refl_equal T (THead (Bind
1445 Abbr) u2 w)) H13 (or_intror (pr0 t1 w) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
1446 (\lambda (y0: T).(subst0 O u2 y0 w))) (ex_intro2 T (\lambda (y0: T).(pr0 t1
1447 y0)) (\lambda (y0: T).(subst0 O u2 y0 w)) t2 H11 H5)))))))))) H7)))))))))))))
1448 (\lambda (b: B).(\lambda (H1: (not (eq B b Abst))).(\lambda (t0: T).(\lambda
1449 (t2: T).(\lambda (H2: (pr0 t0 t2)).(\lambda (H3: (((eq T t0 (THead (Bind
1450 Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2
1451 (THead (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))
1452 (\lambda (u2: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0:
1453 T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t1 (lift (S
1454 O) O t2)))))).(\lambda (u: T).(\lambda (H4: (eq T (THead (Bind b) u (lift (S
1455 O) O t0)) (THead (Bind Abbr) u1 t1))).(let H5 \def (f_equal T B (\lambda (e:
1456 T).(match e in T return (\lambda (_: T).B) with [(TSort _) \Rightarrow b |
1457 (TLRef _) \Rightarrow b | (THead k _ _) \Rightarrow (match k in K return
1458 (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow
1459 b])])) (THead (Bind b) u (lift (S O) O t0)) (THead (Bind Abbr) u1 t1) H4) in
1460 ((let H6 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_:
1461 T).T) with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t _)
1462 \Rightarrow t])) (THead (Bind b) u (lift (S O) O t0)) (THead (Bind Abbr) u1
1463 t1) H4) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e in T return
1464 (\lambda (_: T).T) with [(TSort _) \Rightarrow ((let rec lref_map (f: ((nat
1465 \to nat))) (d: nat) (t: T) on t: T \def (match t with [(TSort n) \Rightarrow
1466 (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with [true
1467 \Rightarrow i | false \Rightarrow (f i)])) | (THead k u0 t3) \Rightarrow
1468 (THead k (lref_map f d u0) (lref_map f (s k d) t3))]) in lref_map) (\lambda
1469 (x0: nat).(plus x0 (S O))) O t0) | (TLRef _) \Rightarrow ((let rec lref_map
1470 (f: ((nat \to nat))) (d: nat) (t: T) on t: T \def (match t with [(TSort n)
1471 \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with
1472 [true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u0 t3)
1473 \Rightarrow (THead k (lref_map f d u0) (lref_map f (s k d) t3))]) in
1474 lref_map) (\lambda (x0: nat).(plus x0 (S O))) O t0) | (THead _ _ t)
1475 \Rightarrow t])) (THead (Bind b) u (lift (S O) O t0)) (THead (Bind Abbr) u1
1476 t1) H4) in (\lambda (_: (eq T u u1)).(\lambda (H9: (eq B b Abbr)).(let H10
1477 \def (eq_ind B b (\lambda (b0: B).(not (eq B b0 Abst))) H1 Abbr H9) in (let
1478 H11 \def (eq_ind_r T t1 (\lambda (t: T).((eq T t0 (THead (Bind Abbr) u1 t))
1479 \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
1480 Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2:
1481 T).(\lambda (t3: T).(or (pr0 t t3) (ex2 T (\lambda (y0: T).(pr0 t y0))
1482 (\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t (lift (S O) O t2))))) H3
1483 (lift (S O) O t0) H7) in (eq_ind T (lift (S O) O t0) (\lambda (t: T).(or
1484 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2
1485 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2:
1486 T).(\lambda (t3: T).(or (pr0 t t3) (ex2 T (\lambda (y0: T).(pr0 t y0))
1487 (\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t (lift (S O) O t2))))
1488 (or_intror (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
1489 Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2:
1490 T).(\lambda (t3: T).(or (pr0 (lift (S O) O t0) t3) (ex2 T (\lambda (y0:
1491 T).(pr0 (lift (S O) O t0) y0)) (\lambda (y0: T).(subst0 O u2 y0 t3)))))))
1492 (pr0 (lift (S O) O t0) (lift (S O) O t2)) (pr0_lift t0 t2 H2 (S O) O)) t1
1493 H7)))))) H6)) H5)))))))))) (\lambda (t0: T).(\lambda (t2: T).(\lambda (_:
1494 (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind Abbr) u1 t1)) \to (or
1495 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2
1496 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2:
1497 T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
1498 (\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t1 (lift (S O) O
1499 t2)))))).(\lambda (u: T).(\lambda (H3: (eq T (THead (Flat Cast) u t0) (THead
1500 (Bind Abbr) u1 t1))).(let H4 \def (eq_ind T (THead (Flat Cast) u t0) (\lambda
1501 (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
1502 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
1503 (match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False |
1504 (Flat _) \Rightarrow True])])) I (THead (Bind Abbr) u1 t1) H3) in (False_ind
1505 (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr)
1506 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2:
1507 T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
1508 (\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t1 (lift (S O) O t2)))
1509 H4)))))))) y x H0))) H)))).
1514 theorem pr0_gen_void:
1515 \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Bind Void) u1
1516 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead
1517 (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
1518 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O x))))))
1520 \lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (H: (pr0 (THead
1521 (Bind Void) u1 t1) x)).(insert_eq T (THead (Bind Void) u1 t1) (\lambda (t:
1522 T).(pr0 t x)) (\lambda (_: T).(or (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
1523 T).(eq T x (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0
1524 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 (lift (S O)
1525 O x)))) (\lambda (y: T).(\lambda (H0: (pr0 y x)).(pr0_ind (\lambda (t:
1526 T).(\lambda (t0: T).((eq T t (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T
1527 (\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead (Bind Void) u2 t2))))
1528 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2:
1529 T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O t0)))))) (\lambda (t: T).(\lambda
1530 (H1: (eq T t (THead (Bind Void) u1 t1))).(let H2 \def (f_equal T T (\lambda
1531 (e: T).e) t (THead (Bind Void) u1 t1) H1) in (eq_ind_r T (THead (Bind Void)
1532 u1 t1) (\lambda (t0: T).(or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq
1533 T t0 (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1
1534 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O
1535 t0)))) (or_introl (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead
1536 (Bind Void) u1 t1) (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_:
1537 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1
1538 (lift (S O) O (THead (Bind Void) u1 t1))) (ex3_2_intro T T (\lambda (u2:
1539 T).(\lambda (t2: T).(eq T (THead (Bind Void) u1 t1) (THead (Bind Void) u2
1540 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
1541 T).(\lambda (t2: T).(pr0 t1 t2))) u1 t1 (refl_equal T (THead (Bind Void) u1
1542 t1)) (pr0_refl u1) (pr0_refl t1))) t H2)))) (\lambda (u0: T).(\lambda (u2:
1543 T).(\lambda (H1: (pr0 u0 u2)).(\lambda (H2: (((eq T u0 (THead (Bind Void) u1
1544 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead
1545 (Bind Void) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
1546 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O
1547 u2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H3: (pr0 t0
1548 t2)).(\lambda (H4: (((eq T t0 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T
1549 (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u3 t3))))
1550 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
1551 T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (k: K).(\lambda
1552 (H5: (eq T (THead k u0 t0) (THead (Bind Void) u1 t1))).(let H6 \def (f_equal
1553 T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with [(TSort _)
1554 \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _) \Rightarrow k0]))
1555 (THead k u0 t0) (THead (Bind Void) u1 t1) H5) in ((let H7 \def (f_equal T T
1556 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
1557 \Rightarrow u0 | (TLRef _) \Rightarrow u0 | (THead _ t _) \Rightarrow t]))
1558 (THead k u0 t0) (THead (Bind Void) u1 t1) H5) in ((let H8 \def (f_equal T T
1559 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
1560 \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) \Rightarrow t]))
1561 (THead k u0 t0) (THead (Bind Void) u1 t1) H5) in (\lambda (H9: (eq T u0
1562 u1)).(\lambda (H10: (eq K k (Bind Void))).(eq_ind_r K (Bind Void) (\lambda
1563 (k0: K).(or (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead k0 u2
1564 t2) (THead (Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1
1565 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O
1566 (THead k0 u2 t2))))) (let H11 \def (eq_ind T t0 (\lambda (t: T).((eq T t
1567 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t3:
1568 T).(eq T t2 (THead (Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda (_:
1569 T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1
1570 (lift (S O) O t2))))) H4 t1 H8) in (let H12 \def (eq_ind T t0 (\lambda (t:
1571 T).(pr0 t t2)) H3 t1 H8) in (let H13 \def (eq_ind T u0 (\lambda (t: T).((eq T
1572 t (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda
1573 (t3: T).(eq T u2 (THead (Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda (_:
1574 T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1
1575 (lift (S O) O u2))))) H2 u1 H9) in (let H14 \def (eq_ind T u0 (\lambda (t:
1576 T).(pr0 t u2)) H1 u1 H9) in (or_introl (ex3_2 T T (\lambda (u3: T).(\lambda
1577 (t3: T).(eq T (THead (Bind Void) u2 t2) (THead (Bind Void) u3 t3)))) (\lambda
1578 (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0
1579 t1 t3)))) (pr0 t1 (lift (S O) O (THead (Bind Void) u2 t2))) (ex3_2_intro T T
1580 (\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind Void) u2 t2) (THead
1581 (Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
1582 (_: T).(\lambda (t3: T).(pr0 t1 t3))) u2 t2 (refl_equal T (THead (Bind Void)
1583 u2 t2)) H14 H12)))))) k H10)))) H7)) H6)))))))))))) (\lambda (u: T).(\lambda
1584 (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1
1585 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
1586 T).(eq T v2 (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_:
1587 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1
1588 (lift (S O) O v2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0
1589 t2)).(\lambda (_: (((eq T t0 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T
1590 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u2 t3))))
1591 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
1592 T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (H5: (eq T (THead
1593 (Flat Appl) v1 (THead (Bind Abst) u t0)) (THead (Bind Void) u1 t1))).(let H6
1594 \def (eq_ind T (THead (Flat Appl) v1 (THead (Bind Abst) u t0)) (\lambda (ee:
1595 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
1596 False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K
1597 return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _)
1598 \Rightarrow True])])) I (THead (Bind Void) u1 t1) H5) in (False_ind (or
1599 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) v2 t2)
1600 (THead (Bind Void) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))
1601 (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O (THead
1602 (Bind Abbr) v2 t2)))) H6)))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B
1603 b Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1
1604 v2)).(\lambda (_: (((eq T v1 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T
1605 (\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Bind Void) u2 t2))))
1606 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2:
1607 T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O v2)))))).(\lambda (u0: T).(\lambda
1608 (u2: T).(\lambda (_: (pr0 u0 u2)).(\lambda (_: (((eq T u0 (THead (Bind Void)
1609 u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead
1610 (Bind Void) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
1611 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O
1612 u2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda
1613 (_: (((eq T t0 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T (\lambda (u3:
1614 T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u3 t3)))) (\lambda (u3:
1615 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
1616 t3)))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (H8: (eq T (THead (Flat Appl)
1617 v1 (THead (Bind b) u0 t0)) (THead (Bind Void) u1 t1))).(let H9 \def (eq_ind T
1618 (THead (Flat Appl) v1 (THead (Bind b) u0 t0)) (\lambda (ee: T).(match ee in T
1619 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
1620 \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda
1621 (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
1622 True])])) I (THead (Bind Void) u1 t1) H8) in (False_ind (or (ex3_2 T T
1623 (\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind b) u2 (THead (Flat Appl)
1624 (lift (S O) O v2) t2)) (THead (Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda
1625 (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1
1626 (lift (S O) O (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)))))
1627 H9))))))))))))))))) (\lambda (u0: T).(\lambda (u2: T).(\lambda (_: (pr0 u0
1628 u2)).(\lambda (_: (((eq T u0 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T
1629 (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead (Bind Void) u3 t2))))
1630 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t2:
1631 T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O u2)))))).(\lambda (t0: T).(\lambda
1632 (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind Void)
1633 u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead
1634 (Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
1635 (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O
1636 t2)))))).(\lambda (w: T).(\lambda (_: (subst0 O u2 t2 w)).(\lambda (H6: (eq T
1637 (THead (Bind Abbr) u0 t0) (THead (Bind Void) u1 t1))).(let H7 \def (eq_ind T
1638 (THead (Bind Abbr) u0 t0) (\lambda (ee: T).(match ee in T return (\lambda (_:
1639 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
1640 (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with
1641 [(Bind b) \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr
1642 \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow False]) | (Flat
1643 _) \Rightarrow False])])) I (THead (Bind Void) u1 t1) H6) in (False_ind (or
1644 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) u2 w)
1645 (THead (Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3)))
1646 (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O (THead
1647 (Bind Abbr) u2 w)))) H7))))))))))))) (\lambda (b: B).(\lambda (H1: (not (eq B
1648 b Abst))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H2: (pr0 t0
1649 t2)).(\lambda (H3: (((eq T t0 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T
1650 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u2 t3))))
1651 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
1652 T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (u: T).(\lambda
1653 (H4: (eq T (THead (Bind b) u (lift (S O) O t0)) (THead (Bind Void) u1
1654 t1))).(let H5 \def (f_equal T B (\lambda (e: T).(match e in T return (\lambda
1655 (_: T).B) with [(TSort _) \Rightarrow b | (TLRef _) \Rightarrow b | (THead k
1656 _ _) \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b0)
1657 \Rightarrow b0 | (Flat _) \Rightarrow b])])) (THead (Bind b) u (lift (S O) O
1658 t0)) (THead (Bind Void) u1 t1) H4) in ((let H6 \def (f_equal T T (\lambda (e:
1659 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u |
1660 (TLRef _) \Rightarrow u | (THead _ t _) \Rightarrow t])) (THead (Bind b) u
1661 (lift (S O) O t0)) (THead (Bind Void) u1 t1) H4) in ((let H7 \def (f_equal T
1662 T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
1663 \Rightarrow ((let rec lref_map (f: ((nat \to nat))) (d: nat) (t: T) on t: T
1664 \def (match t with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow
1665 (TLRef (match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)]))
1666 | (THead k u0 t3) \Rightarrow (THead k (lref_map f d u0) (lref_map f (s k d)
1667 t3))]) in lref_map) (\lambda (x0: nat).(plus x0 (S O))) O t0) | (TLRef _)
1668 \Rightarrow ((let rec lref_map (f: ((nat \to nat))) (d: nat) (t: T) on t: T
1669 \def (match t with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow
1670 (TLRef (match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)]))
1671 | (THead k u0 t3) \Rightarrow (THead k (lref_map f d u0) (lref_map f (s k d)
1672 t3))]) in lref_map) (\lambda (x0: nat).(plus x0 (S O))) O t0) | (THead _ _ t)
1673 \Rightarrow t])) (THead (Bind b) u (lift (S O) O t0)) (THead (Bind Void) u1
1674 t1) H4) in (\lambda (_: (eq T u u1)).(\lambda (H9: (eq B b Void)).(let H10
1675 \def (eq_ind B b (\lambda (b0: B).(not (eq B b0 Abst))) H1 Void H9) in (let
1676 H11 \def (eq_ind_r T t1 (\lambda (t: T).((eq T t0 (THead (Bind Void) u1 t))
1677 \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
1678 Void) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
1679 T).(\lambda (t3: T).(pr0 t t3)))) (pr0 t (lift (S O) O t2))))) H3 (lift (S O)
1680 O t0) H7) in (eq_ind T (lift (S O) O t0) (\lambda (t: T).(or (ex3_2 T T
1681 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u2 t3))))
1682 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
1683 T).(pr0 t t3)))) (pr0 t (lift (S O) O t2)))) (or_intror (ex3_2 T T (\lambda
1684 (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u2 t3)))) (\lambda (u2:
1685 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 (lift
1686 (S O) O t0) t3)))) (pr0 (lift (S O) O t0) (lift (S O) O t2)) (pr0_lift t0 t2
1687 H2 (S O) O)) t1 H7)))))) H6)) H5)))))))))) (\lambda (t0: T).(\lambda (t2:
1688 T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind Void) u1
1689 t1)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead
1690 (Bind Void) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
1691 (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O
1692 t2)))))).(\lambda (u: T).(\lambda (H3: (eq T (THead (Flat Cast) u t0) (THead
1693 (Bind Void) u1 t1))).(let H4 \def (eq_ind T (THead (Flat Cast) u t0) (\lambda
1694 (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
1695 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
1696 (match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False |
1697 (Flat _) \Rightarrow True])])) I (THead (Bind Void) u1 t1) H3) in (False_ind
1698 (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void)
1699 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
1700 T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O t2))) H4)))))))) y x
1706 theorem pr0_gen_lift:
1707 \forall (t1: T).(\forall (x: T).(\forall (h: nat).(\forall (d: nat).((pr0
1708 (lift h d t1) x) \to (ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda
1709 (t2: T).(pr0 t1 t2)))))))
1711 \lambda (t1: T).(\lambda (x: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda
1712 (H: (pr0 (lift h d t1) x)).(insert_eq T (lift h d t1) (\lambda (t: T).(pr0 t
1713 x)) (\lambda (_: T).(ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda
1714 (t2: T).(pr0 t1 t2)))) (\lambda (y: T).(\lambda (H0: (pr0 y x)).(unintro nat
1715 d (\lambda (n: nat).((eq T y (lift h n t1)) \to (ex2 T (\lambda (t2: T).(eq T
1716 x (lift h n t2))) (\lambda (t2: T).(pr0 t1 t2))))) (unintro T t1 (\lambda (t:
1717 T).(\forall (x0: nat).((eq T y (lift h x0 t)) \to (ex2 T (\lambda (t2: T).(eq
1718 T x (lift h x0 t2))) (\lambda (t2: T).(pr0 t t2)))))) (pr0_ind (\lambda (t:
1719 T).(\lambda (t0: T).(\forall (x0: T).(\forall (x1: nat).((eq T t (lift h x1
1720 x0)) \to (ex2 T (\lambda (t2: T).(eq T t0 (lift h x1 t2))) (\lambda (t2:
1721 T).(pr0 x0 t2)))))))) (\lambda (t: T).(\lambda (x0: T).(\lambda (x1:
1722 nat).(\lambda (H1: (eq T t (lift h x1 x0))).(ex_intro2 T (\lambda (t2: T).(eq
1723 T t (lift h x1 t2))) (\lambda (t2: T).(pr0 x0 t2)) x0 H1 (pr0_refl x0))))))
1724 (\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (H2:
1725 ((\forall (x0: T).(\forall (x1: nat).((eq T u1 (lift h x1 x0)) \to (ex2 T
1726 (\lambda (t2: T).(eq T u2 (lift h x1 t2))) (\lambda (t2: T).(pr0 x0
1727 t2)))))))).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (pr0 t2
1728 t3)).(\lambda (H4: ((\forall (x0: T).(\forall (x1: nat).((eq T t2 (lift h x1
1729 x0)) \to (ex2 T (\lambda (t4: T).(eq T t3 (lift h x1 t4))) (\lambda (t4:
1730 T).(pr0 x0 t4)))))))).(\lambda (k: K).(\lambda (x0: T).(\lambda (x1:
1731 nat).(\lambda (H5: (eq T (THead k u1 t2) (lift h x1 x0))).(K_ind (\lambda
1732 (k0: K).((eq T (THead k0 u1 t2) (lift h x1 x0)) \to (ex2 T (\lambda (t4:
1733 T).(eq T (THead k0 u2 t3) (lift h x1 t4))) (\lambda (t4: T).(pr0 x0 t4)))))
1734 (\lambda (b: B).(\lambda (H6: (eq T (THead (Bind b) u1 t2) (lift h x1
1735 x0))).(ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T x0 (THead (Bind
1736 b) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T u1 (lift h x1 y0))))
1737 (\lambda (_: T).(\lambda (z: T).(eq T t2 (lift h (S x1) z)))) (ex2 T (\lambda
1738 (t4: T).(eq T (THead (Bind b) u2 t3) (lift h x1 t4))) (\lambda (t4: T).(pr0
1739 x0 t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H7: (eq T x0 (THead
1740 (Bind b) x2 x3))).(\lambda (H8: (eq T u1 (lift h x1 x2))).(\lambda (H9: (eq T
1741 t2 (lift h (S x1) x3))).(eq_ind_r T (THead (Bind b) x2 x3) (\lambda (t:
1742 T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind b) u2 t3) (lift h x1 t4)))
1743 (\lambda (t4: T).(pr0 t t4)))) (ex2_ind T (\lambda (t4: T).(eq T t3 (lift h
1744 (S x1) t4))) (\lambda (t4: T).(pr0 x3 t4)) (ex2 T (\lambda (t4: T).(eq T
1745 (THead (Bind b) u2 t3) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind b)
1746 x2 x3) t4))) (\lambda (x4: T).(\lambda (H_x: (eq T t3 (lift h (S x1)
1747 x4))).(\lambda (H10: (pr0 x3 x4)).(eq_ind_r T (lift h (S x1) x4) (\lambda (t:
1748 T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind b) u2 t) (lift h x1 t4)))
1749 (\lambda (t4: T).(pr0 (THead (Bind b) x2 x3) t4)))) (ex2_ind T (\lambda (t4:
1750 T).(eq T u2 (lift h x1 t4))) (\lambda (t4: T).(pr0 x2 t4)) (ex2 T (\lambda
1751 (t4: T).(eq T (THead (Bind b) u2 (lift h (S x1) x4)) (lift h x1 t4)))
1752 (\lambda (t4: T).(pr0 (THead (Bind b) x2 x3) t4))) (\lambda (x5: T).(\lambda
1753 (H_x0: (eq T u2 (lift h x1 x5))).(\lambda (H11: (pr0 x2 x5)).(eq_ind_r T
1754 (lift h x1 x5) (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind b)
1755 t (lift h (S x1) x4)) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind b)
1756 x2 x3) t4)))) (ex_intro2 T (\lambda (t4: T).(eq T (THead (Bind b) (lift h x1
1757 x5) (lift h (S x1) x4)) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind
1758 b) x2 x3) t4)) (THead (Bind b) x5 x4) (sym_eq T (lift h x1 (THead (Bind b) x5
1759 x4)) (THead (Bind b) (lift h x1 x5) (lift h (S x1) x4)) (lift_bind b x5 x4 h
1760 x1)) (pr0_comp x2 x5 H11 x3 x4 H10 (Bind b))) u2 H_x0)))) (H2 x2 x1 H8)) t3
1761 H_x)))) (H4 x3 (S x1) H9)) x0 H7)))))) (lift_gen_bind b u1 t2 x0 h x1 H6))))
1762 (\lambda (f: F).(\lambda (H6: (eq T (THead (Flat f) u1 t2) (lift h x1
1763 x0))).(ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T x0 (THead (Flat
1764 f) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T u1 (lift h x1 y0))))
1765 (\lambda (_: T).(\lambda (z: T).(eq T t2 (lift h x1 z)))) (ex2 T (\lambda
1766 (t4: T).(eq T (THead (Flat f) u2 t3) (lift h x1 t4))) (\lambda (t4: T).(pr0
1767 x0 t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H7: (eq T x0 (THead
1768 (Flat f) x2 x3))).(\lambda (H8: (eq T u1 (lift h x1 x2))).(\lambda (H9: (eq T
1769 t2 (lift h x1 x3))).(eq_ind_r T (THead (Flat f) x2 x3) (\lambda (t: T).(ex2 T
1770 (\lambda (t4: T).(eq T (THead (Flat f) u2 t3) (lift h x1 t4))) (\lambda (t4:
1771 T).(pr0 t t4)))) (ex2_ind T (\lambda (t4: T).(eq T t3 (lift h x1 t4)))
1772 (\lambda (t4: T).(pr0 x3 t4)) (ex2 T (\lambda (t4: T).(eq T (THead (Flat f)
1773 u2 t3) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat f) x2 x3) t4)))
1774 (\lambda (x4: T).(\lambda (H_x: (eq T t3 (lift h x1 x4))).(\lambda (H10: (pr0
1775 x3 x4)).(eq_ind_r T (lift h x1 x4) (\lambda (t: T).(ex2 T (\lambda (t4:
1776 T).(eq T (THead (Flat f) u2 t) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead
1777 (Flat f) x2 x3) t4)))) (ex2_ind T (\lambda (t4: T).(eq T u2 (lift h x1 t4)))
1778 (\lambda (t4: T).(pr0 x2 t4)) (ex2 T (\lambda (t4: T).(eq T (THead (Flat f)
1779 u2 (lift h x1 x4)) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat f) x2
1780 x3) t4))) (\lambda (x5: T).(\lambda (H_x0: (eq T u2 (lift h x1 x5))).(\lambda
1781 (H11: (pr0 x2 x5)).(eq_ind_r T (lift h x1 x5) (\lambda (t: T).(ex2 T (\lambda
1782 (t4: T).(eq T (THead (Flat f) t (lift h x1 x4)) (lift h x1 t4))) (\lambda
1783 (t4: T).(pr0 (THead (Flat f) x2 x3) t4)))) (ex_intro2 T (\lambda (t4: T).(eq
1784 T (THead (Flat f) (lift h x1 x5) (lift h x1 x4)) (lift h x1 t4))) (\lambda
1785 (t4: T).(pr0 (THead (Flat f) x2 x3) t4)) (THead (Flat f) x5 x4) (sym_eq T
1786 (lift h x1 (THead (Flat f) x5 x4)) (THead (Flat f) (lift h x1 x5) (lift h x1
1787 x4)) (lift_flat f x5 x4 h x1)) (pr0_comp x2 x5 H11 x3 x4 H10 (Flat f))) u2
1788 H_x0)))) (H2 x2 x1 H8)) t3 H_x)))) (H4 x3 x1 H9)) x0 H7)))))) (lift_gen_flat
1789 f u1 t2 x0 h x1 H6)))) k H5))))))))))))) (\lambda (u: T).(\lambda (v1:
1790 T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (H2: ((\forall (x0:
1791 T).(\forall (x1: nat).((eq T v1 (lift h x1 x0)) \to (ex2 T (\lambda (t2:
1792 T).(eq T v2 (lift h x1 t2))) (\lambda (t2: T).(pr0 x0 t2)))))))).(\lambda
1793 (t2: T).(\lambda (t3: T).(\lambda (_: (pr0 t2 t3)).(\lambda (H4: ((\forall
1794 (x0: T).(\forall (x1: nat).((eq T t2 (lift h x1 x0)) \to (ex2 T (\lambda (t4:
1795 T).(eq T t3 (lift h x1 t4))) (\lambda (t4: T).(pr0 x0 t4)))))))).(\lambda
1796 (x0: T).(\lambda (x1: nat).(\lambda (H5: (eq T (THead (Flat Appl) v1 (THead
1797 (Bind Abst) u t2)) (lift h x1 x0))).(ex3_2_ind T T (\lambda (y0: T).(\lambda
1798 (z: T).(eq T x0 (THead (Flat Appl) y0 z)))) (\lambda (y0: T).(\lambda (_:
1799 T).(eq T v1 (lift h x1 y0)))) (\lambda (_: T).(\lambda (z: T).(eq T (THead
1800 (Bind Abst) u t2) (lift h x1 z)))) (ex2 T (\lambda (t4: T).(eq T (THead (Bind
1801 Abbr) v2 t3) (lift h x1 t4))) (\lambda (t4: T).(pr0 x0 t4))) (\lambda (x2:
1802 T).(\lambda (x3: T).(\lambda (H6: (eq T x0 (THead (Flat Appl) x2
1803 x3))).(\lambda (H7: (eq T v1 (lift h x1 x2))).(\lambda (H8: (eq T (THead
1804 (Bind Abst) u t2) (lift h x1 x3))).(eq_ind_r T (THead (Flat Appl) x2 x3)
1805 (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind Abbr) v2 t3) (lift
1806 h x1 t4))) (\lambda (t4: T).(pr0 t t4)))) (ex3_2_ind T T (\lambda (y0:
1807 T).(\lambda (z: T).(eq T x3 (THead (Bind Abst) y0 z)))) (\lambda (y0:
1808 T).(\lambda (_: T).(eq T u (lift h x1 y0)))) (\lambda (_: T).(\lambda (z:
1809 T).(eq T t2 (lift h (S x1) z)))) (ex2 T (\lambda (t4: T).(eq T (THead (Bind
1810 Abbr) v2 t3) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat Appl) x2 x3)
1811 t4))) (\lambda (x4: T).(\lambda (x5: T).(\lambda (H9: (eq T x3 (THead (Bind
1812 Abst) x4 x5))).(\lambda (_: (eq T u (lift h x1 x4))).(\lambda (H11: (eq T t2
1813 (lift h (S x1) x5))).(eq_ind_r T (THead (Bind Abst) x4 x5) (\lambda (t:
1814 T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4)))
1815 (\lambda (t4: T).(pr0 (THead (Flat Appl) x2 t) t4)))) (ex2_ind T (\lambda
1816 (t4: T).(eq T t3 (lift h (S x1) t4))) (\lambda (t4: T).(pr0 x5 t4)) (ex2 T
1817 (\lambda (t4: T).(eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4))) (\lambda
1818 (t4: T).(pr0 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5)) t4))) (\lambda
1819 (x6: T).(\lambda (H_x: (eq T t3 (lift h (S x1) x6))).(\lambda (H12: (pr0 x5
1820 x6)).(eq_ind_r T (lift h (S x1) x6) (\lambda (t: T).(ex2 T (\lambda (t4:
1821 T).(eq T (THead (Bind Abbr) v2 t) (lift h x1 t4))) (\lambda (t4: T).(pr0
1822 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5)) t4)))) (ex2_ind T (\lambda
1823 (t4: T).(eq T v2 (lift h x1 t4))) (\lambda (t4: T).(pr0 x2 t4)) (ex2 T
1824 (\lambda (t4: T).(eq T (THead (Bind Abbr) v2 (lift h (S x1) x6)) (lift h x1
1825 t4))) (\lambda (t4: T).(pr0 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5))
1826 t4))) (\lambda (x7: T).(\lambda (H_x0: (eq T v2 (lift h x1 x7))).(\lambda
1827 (H13: (pr0 x2 x7)).(eq_ind_r T (lift h x1 x7) (\lambda (t: T).(ex2 T (\lambda
1828 (t4: T).(eq T (THead (Bind Abbr) t (lift h (S x1) x6)) (lift h x1 t4)))
1829 (\lambda (t4: T).(pr0 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5)) t4))))
1830 (ex_intro2 T (\lambda (t4: T).(eq T (THead (Bind Abbr) (lift h x1 x7) (lift h
1831 (S x1) x6)) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat Appl) x2
1832 (THead (Bind Abst) x4 x5)) t4)) (THead (Bind Abbr) x7 x6) (sym_eq T (lift h
1833 x1 (THead (Bind Abbr) x7 x6)) (THead (Bind Abbr) (lift h x1 x7) (lift h (S
1834 x1) x6)) (lift_bind Abbr x7 x6 h x1)) (pr0_beta x4 x2 x7 H13 x5 x6 H12)) v2
1835 H_x0)))) (H2 x2 x1 H7)) t3 H_x)))) (H4 x5 (S x1) H11)) x3 H9))))))
1836 (lift_gen_bind Abst u t2 x3 h x1 H8)) x0 H6)))))) (lift_gen_flat Appl v1
1837 (THead (Bind Abst) u t2) x0 h x1 H5)))))))))))))) (\lambda (b: B).(\lambda
1838 (H1: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0
1839 v1 v2)).(\lambda (H3: ((\forall (x0: T).(\forall (x1: nat).((eq T v1 (lift h
1840 x1 x0)) \to (ex2 T (\lambda (t2: T).(eq T v2 (lift h x1 t2))) (\lambda (t2:
1841 T).(pr0 x0 t2)))))))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1
1842 u2)).(\lambda (H5: ((\forall (x0: T).(\forall (x1: nat).((eq T u1 (lift h x1
1843 x0)) \to (ex2 T (\lambda (t2: T).(eq T u2 (lift h x1 t2))) (\lambda (t2:
1844 T).(pr0 x0 t2)))))))).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (pr0 t2
1845 t3)).(\lambda (H7: ((\forall (x0: T).(\forall (x1: nat).((eq T t2 (lift h x1
1846 x0)) \to (ex2 T (\lambda (t4: T).(eq T t3 (lift h x1 t4))) (\lambda (t4:
1847 T).(pr0 x0 t4)))))))).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H8: (eq T
1848 (THead (Flat Appl) v1 (THead (Bind b) u1 t2)) (lift h x1 x0))).(ex3_2_ind T T
1849 (\lambda (y0: T).(\lambda (z: T).(eq T x0 (THead (Flat Appl) y0 z))))
1850 (\lambda (y0: T).(\lambda (_: T).(eq T v1 (lift h x1 y0)))) (\lambda (_:
1851 T).(\lambda (z: T).(eq T (THead (Bind b) u1 t2) (lift h x1 z)))) (ex2 T
1852 (\lambda (t4: T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O
1853 v2) t3)) (lift h x1 t4))) (\lambda (t4: T).(pr0 x0 t4))) (\lambda (x2:
1854 T).(\lambda (x3: T).(\lambda (H9: (eq T x0 (THead (Flat Appl) x2
1855 x3))).(\lambda (H10: (eq T v1 (lift h x1 x2))).(\lambda (H11: (eq T (THead
1856 (Bind b) u1 t2) (lift h x1 x3))).(eq_ind_r T (THead (Flat Appl) x2 x3)
1857 (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind b) u2 (THead (Flat
1858 Appl) (lift (S O) O v2) t3)) (lift h x1 t4))) (\lambda (t4: T).(pr0 t t4))))
1859 (ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T x3 (THead (Bind b) y0
1860 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T u1 (lift h x1 y0)))) (\lambda
1861 (_: T).(\lambda (z: T).(eq T t2 (lift h (S x1) z)))) (ex2 T (\lambda (t4:
1862 T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)) (lift h
1863 x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat Appl) x2 x3) t4))) (\lambda (x4:
1864 T).(\lambda (x5: T).(\lambda (H12: (eq T x3 (THead (Bind b) x4 x5))).(\lambda
1865 (H13: (eq T u1 (lift h x1 x4))).(\lambda (H14: (eq T t2 (lift h (S x1)
1866 x5))).(eq_ind_r T (THead (Bind b) x4 x5) (\lambda (t: T).(ex2 T (\lambda (t4:
1867 T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)) (lift h
1868 x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat Appl) x2 t) t4)))) (ex2_ind T
1869 (\lambda (t4: T).(eq T t3 (lift h (S x1) t4))) (\lambda (t4: T).(pr0 x5 t4))
1870 (ex2 T (\lambda (t4: T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S
1871 O) O v2) t3)) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat Appl) x2
1872 (THead (Bind b) x4 x5)) t4))) (\lambda (x6: T).(\lambda (H_x: (eq T t3 (lift
1873 h (S x1) x6))).(\lambda (H15: (pr0 x5 x6)).(eq_ind_r T (lift h (S x1) x6)
1874 (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind b) u2 (THead (Flat
1875 Appl) (lift (S O) O v2) t)) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead
1876 (Flat Appl) x2 (THead (Bind b) x4 x5)) t4)))) (ex2_ind T (\lambda (t4: T).(eq
1877 T u2 (lift h x1 t4))) (\lambda (t4: T).(pr0 x4 t4)) (ex2 T (\lambda (t4:
1878 T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) (lift h (S
1879 x1) x6))) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat Appl) x2 (THead
1880 (Bind b) x4 x5)) t4))) (\lambda (x7: T).(\lambda (H_x0: (eq T u2 (lift h x1
1881 x7))).(\lambda (H16: (pr0 x4 x7)).(eq_ind_r T (lift h x1 x7) (\lambda (t:
1882 T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind b) t (THead (Flat Appl) (lift
1883 (S O) O v2) (lift h (S x1) x6))) (lift h x1 t4))) (\lambda (t4: T).(pr0
1884 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4)))) (ex2_ind T (\lambda (t4:
1885 T).(eq T v2 (lift h x1 t4))) (\lambda (t4: T).(pr0 x2 t4)) (ex2 T (\lambda
1886 (t4: T).(eq T (THead (Bind b) (lift h x1 x7) (THead (Flat Appl) (lift (S O) O
1887 v2) (lift h (S x1) x6))) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat
1888 Appl) x2 (THead (Bind b) x4 x5)) t4))) (\lambda (x8: T).(\lambda (H_x1: (eq T
1889 v2 (lift h x1 x8))).(\lambda (H17: (pr0 x2 x8)).(eq_ind_r T (lift h x1 x8)
1890 (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind b) (lift h x1 x7)
1891 (THead (Flat Appl) (lift (S O) O t) (lift h (S x1) x6))) (lift h x1 t4)))
1892 (\lambda (t4: T).(pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4))))
1893 (eq_ind T (lift h (plus (S O) x1) (lift (S O) O x8)) (\lambda (t: T).(ex2 T
1894 (\lambda (t4: T).(eq T (THead (Bind b) (lift h x1 x7) (THead (Flat Appl) t
1895 (lift h (S x1) x6))) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat
1896 Appl) x2 (THead (Bind b) x4 x5)) t4)))) (eq_ind T (lift h (S x1) (THead (Flat
1897 Appl) (lift (S O) O x8) x6)) (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T
1898 (THead (Bind b) (lift h x1 x7) t) (lift h x1 t4))) (\lambda (t4: T).(pr0
1899 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4)))) (ex_intro2 T (\lambda
1900 (t4: T).(eq T (THead (Bind b) (lift h x1 x7) (lift h (S x1) (THead (Flat
1901 Appl) (lift (S O) O x8) x6))) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead
1902 (Flat Appl) x2 (THead (Bind b) x4 x5)) t4)) (THead (Bind b) x7 (THead (Flat
1903 Appl) (lift (S O) O x8) x6)) (sym_eq T (lift h x1 (THead (Bind b) x7 (THead
1904 (Flat Appl) (lift (S O) O x8) x6))) (THead (Bind b) (lift h x1 x7) (lift h (S
1905 x1) (THead (Flat Appl) (lift (S O) O x8) x6))) (lift_bind b x7 (THead (Flat
1906 Appl) (lift (S O) O x8) x6) h x1)) (pr0_upsilon b H1 x2 x8 H17 x4 x7 H16 x5
1907 x6 H15)) (THead (Flat Appl) (lift h (S x1) (lift (S O) O x8)) (lift h (S x1)
1908 x6)) (lift_flat Appl (lift (S O) O x8) x6 h (S x1))) (lift (S O) O (lift h x1
1909 x8)) (lift_d x8 h (S O) x1 O (le_O_n x1))) v2 H_x1)))) (H3 x2 x1 H10)) u2
1910 H_x0)))) (H5 x4 x1 H13)) t3 H_x)))) (H7 x5 (S x1) H14)) x3 H12))))))
1911 (lift_gen_bind b u1 t2 x3 h x1 H11)) x0 H9)))))) (lift_gen_flat Appl v1
1912 (THead (Bind b) u1 t2) x0 h x1 H8))))))))))))))))))) (\lambda (u1:
1913 T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (H2: ((\forall (x0:
1914 T).(\forall (x1: nat).((eq T u1 (lift h x1 x0)) \to (ex2 T (\lambda (t2:
1915 T).(eq T u2 (lift h x1 t2))) (\lambda (t2: T).(pr0 x0 t2)))))))).(\lambda
1916 (t2: T).(\lambda (t3: T).(\lambda (_: (pr0 t2 t3)).(\lambda (H4: ((\forall
1917 (x0: T).(\forall (x1: nat).((eq T t2 (lift h x1 x0)) \to (ex2 T (\lambda (t4:
1918 T).(eq T t3 (lift h x1 t4))) (\lambda (t4: T).(pr0 x0 t4)))))))).(\lambda (w:
1919 T).(\lambda (H5: (subst0 O u2 t3 w)).(\lambda (x0: T).(\lambda (x1:
1920 nat).(\lambda (H6: (eq T (THead (Bind Abbr) u1 t2) (lift h x1
1921 x0))).(ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T x0 (THead (Bind
1922 Abbr) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T u1 (lift h x1 y0))))
1923 (\lambda (_: T).(\lambda (z: T).(eq T t2 (lift h (S x1) z)))) (ex2 T (\lambda
1924 (t4: T).(eq T (THead (Bind Abbr) u2 w) (lift h x1 t4))) (\lambda (t4: T).(pr0
1925 x0 t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H7: (eq T x0 (THead
1926 (Bind Abbr) x2 x3))).(\lambda (H8: (eq T u1 (lift h x1 x2))).(\lambda (H9:
1927 (eq T t2 (lift h (S x1) x3))).(eq_ind_r T (THead (Bind Abbr) x2 x3) (\lambda
1928 (t: T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind Abbr) u2 w) (lift h x1
1929 t4))) (\lambda (t4: T).(pr0 t t4)))) (ex2_ind T (\lambda (t4: T).(eq T t3
1930 (lift h (S x1) t4))) (\lambda (t4: T).(pr0 x3 t4)) (ex2 T (\lambda (t4:
1931 T).(eq T (THead (Bind Abbr) u2 w) (lift h x1 t4))) (\lambda (t4: T).(pr0
1932 (THead (Bind Abbr) x2 x3) t4))) (\lambda (x4: T).(\lambda (H_x: (eq T t3
1933 (lift h (S x1) x4))).(\lambda (H10: (pr0 x3 x4)).(let H11 \def (eq_ind T t3
1934 (\lambda (t: T).(subst0 O u2 t w)) H5 (lift h (S x1) x4) H_x) in (ex2_ind T
1935 (\lambda (t4: T).(eq T u2 (lift h x1 t4))) (\lambda (t4: T).(pr0 x2 t4)) (ex2
1936 T (\lambda (t4: T).(eq T (THead (Bind Abbr) u2 w) (lift h x1 t4))) (\lambda
1937 (t4: T).(pr0 (THead (Bind Abbr) x2 x3) t4))) (\lambda (x5: T).(\lambda (H_x0:
1938 (eq T u2 (lift h x1 x5))).(\lambda (H12: (pr0 x2 x5)).(eq_ind_r T (lift h x1
1939 x5) (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind Abbr) t w)
1940 (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind Abbr) x2 x3) t4)))) (let
1941 H13 \def (eq_ind T u2 (\lambda (t: T).(subst0 O t (lift h (S x1) x4) w)) H11
1942 (lift h x1 x5) H_x0) in (let H14 \def (refl_equal nat (S (plus O x1))) in
1943 (let H15 \def (eq_ind nat (S x1) (\lambda (n: nat).(subst0 O (lift h x1 x5)
1944 (lift h n x4) w)) H13 (S (plus O x1)) H14) in (ex2_ind T (\lambda (t4: T).(eq
1945 T w (lift h (S (plus O x1)) t4))) (\lambda (t4: T).(subst0 O x5 x4 t4)) (ex2
1946 T (\lambda (t4: T).(eq T (THead (Bind Abbr) (lift h x1 x5) w) (lift h x1
1947 t4))) (\lambda (t4: T).(pr0 (THead (Bind Abbr) x2 x3) t4))) (\lambda (x6:
1948 T).(\lambda (H16: (eq T w (lift h (S (plus O x1)) x6))).(\lambda (H17:
1949 (subst0 O x5 x4 x6)).(eq_ind_r T (lift h (S (plus O x1)) x6) (\lambda (t:
1950 T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind Abbr) (lift h x1 x5) t) (lift h
1951 x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind Abbr) x2 x3) t4)))) (ex_intro2 T
1952 (\lambda (t4: T).(eq T (THead (Bind Abbr) (lift h x1 x5) (lift h (S (plus O
1953 x1)) x6)) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind Abbr) x2 x3)
1954 t4)) (THead (Bind Abbr) x5 x6) (sym_eq T (lift h x1 (THead (Bind Abbr) x5
1955 x6)) (THead (Bind Abbr) (lift h x1 x5) (lift h (S (plus O x1)) x6))
1956 (lift_bind Abbr x5 x6 h (plus O x1))) (pr0_delta x2 x5 H12 x3 x4 H10 x6 H17))
1957 w H16)))) (subst0_gen_lift_lt x5 x4 w O h x1 H15))))) u2 H_x0)))) (H2 x2 x1
1958 H8)))))) (H4 x3 (S x1) H9)) x0 H7)))))) (lift_gen_bind Abbr u1 t2 x0 h x1
1959 H6))))))))))))))) (\lambda (b: B).(\lambda (H1: (not (eq B b Abst))).(\lambda
1960 (t2: T).(\lambda (t3: T).(\lambda (_: (pr0 t2 t3)).(\lambda (H3: ((\forall
1961 (x0: T).(\forall (x1: nat).((eq T t2 (lift h x1 x0)) \to (ex2 T (\lambda (t4:
1962 T).(eq T t3 (lift h x1 t4))) (\lambda (t4: T).(pr0 x0 t4)))))))).(\lambda (u:
1963 T).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H4: (eq T (THead (Bind b) u
1964 (lift (S O) O t2)) (lift h x1 x0))).(ex3_2_ind T T (\lambda (y0: T).(\lambda
1965 (z: T).(eq T x0 (THead (Bind b) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq
1966 T u (lift h x1 y0)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift (S O) O t2)
1967 (lift h (S x1) z)))) (ex2 T (\lambda (t4: T).(eq T t3 (lift h x1 t4)))
1968 (\lambda (t4: T).(pr0 x0 t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda
1969 (H5: (eq T x0 (THead (Bind b) x2 x3))).(\lambda (_: (eq T u (lift h x1
1970 x2))).(\lambda (H7: (eq T (lift (S O) O t2) (lift h (S x1) x3))).(eq_ind_r T
1971 (THead (Bind b) x2 x3) (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T t3 (lift
1972 h x1 t4))) (\lambda (t4: T).(pr0 t t4)))) (let H8 \def (eq_ind_r nat (plus (S
1973 O) x1) (\lambda (n: nat).(eq nat (S x1) n)) (refl_equal nat (plus (S O) x1))
1974 (plus x1 (S O)) (plus_sym x1 (S O))) in (let H9 \def (eq_ind nat (S x1)
1975 (\lambda (n: nat).(eq T (lift (S O) O t2) (lift h n x3))) H7 (plus x1 (S O))
1976 H8) in (ex2_ind T (\lambda (t4: T).(eq T x3 (lift (S O) O t4))) (\lambda (t4:
1977 T).(eq T t2 (lift h x1 t4))) (ex2 T (\lambda (t4: T).(eq T t3 (lift h x1
1978 t4))) (\lambda (t4: T).(pr0 (THead (Bind b) x2 x3) t4))) (\lambda (x4:
1979 T).(\lambda (H10: (eq T x3 (lift (S O) O x4))).(\lambda (H11: (eq T t2 (lift
1980 h x1 x4))).(eq_ind_r T (lift (S O) O x4) (\lambda (t: T).(ex2 T (\lambda (t4:
1981 T).(eq T t3 (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind b) x2 t)
1982 t4)))) (ex2_ind T (\lambda (t4: T).(eq T t3 (lift h x1 t4))) (\lambda (t4:
1983 T).(pr0 x4 t4)) (ex2 T (\lambda (t4: T).(eq T t3 (lift h x1 t4))) (\lambda
1984 (t4: T).(pr0 (THead (Bind b) x2 (lift (S O) O x4)) t4))) (\lambda (x5:
1985 T).(\lambda (H_x: (eq T t3 (lift h x1 x5))).(\lambda (H12: (pr0 x4
1986 x5)).(eq_ind_r T (lift h x1 x5) (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T
1987 t (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind b) x2 (lift (S O) O
1988 x4)) t4)))) (ex_intro2 T (\lambda (t4: T).(eq T (lift h x1 x5) (lift h x1
1989 t4))) (\lambda (t4: T).(pr0 (THead (Bind b) x2 (lift (S O) O x4)) t4)) x5
1990 (refl_equal T (lift h x1 x5)) (pr0_zeta b H1 x4 x5 H12 x2)) t3 H_x)))) (H3 x4
1991 x1 H11)) x3 H10)))) (lift_gen_lift t2 x3 (S O) h O x1 (le_O_n x1) H9)))) x0
1992 H5)))))) (lift_gen_bind b u (lift (S O) O t2) x0 h x1 H4)))))))))))) (\lambda
1993 (t2: T).(\lambda (t3: T).(\lambda (_: (pr0 t2 t3)).(\lambda (H2: ((\forall
1994 (x0: T).(\forall (x1: nat).((eq T t2 (lift h x1 x0)) \to (ex2 T (\lambda (t4:
1995 T).(eq T t3 (lift h x1 t4))) (\lambda (t4: T).(pr0 x0 t4)))))))).(\lambda (u:
1996 T).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H3: (eq T (THead (Flat Cast)
1997 u t2) (lift h x1 x0))).(ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T
1998 x0 (THead (Flat Cast) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T u (lift
1999 h x1 y0)))) (\lambda (_: T).(\lambda (z: T).(eq T t2 (lift h x1 z)))) (ex2 T
2000 (\lambda (t4: T).(eq T t3 (lift h x1 t4))) (\lambda (t4: T).(pr0 x0 t4)))
2001 (\lambda (x2: T).(\lambda (x3: T).(\lambda (H4: (eq T x0 (THead (Flat Cast)
2002 x2 x3))).(\lambda (_: (eq T u (lift h x1 x2))).(\lambda (H6: (eq T t2 (lift h
2003 x1 x3))).(eq_ind_r T (THead (Flat Cast) x2 x3) (\lambda (t: T).(ex2 T
2004 (\lambda (t4: T).(eq T t3 (lift h x1 t4))) (\lambda (t4: T).(pr0 t t4))))
2005 (ex2_ind T (\lambda (t4: T).(eq T t3 (lift h x1 t4))) (\lambda (t4: T).(pr0
2006 x3 t4)) (ex2 T (\lambda (t4: T).(eq T t3 (lift h x1 t4))) (\lambda (t4:
2007 T).(pr0 (THead (Flat Cast) x2 x3) t4))) (\lambda (x4: T).(\lambda (H_x: (eq T
2008 t3 (lift h x1 x4))).(\lambda (H7: (pr0 x3 x4)).(eq_ind_r T (lift h x1 x4)
2009 (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T t (lift h x1 t4))) (\lambda
2010 (t4: T).(pr0 (THead (Flat Cast) x2 x3) t4)))) (ex_intro2 T (\lambda (t4:
2011 T).(eq T (lift h x1 x4) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat
2012 Cast) x2 x3) t4)) x4 (refl_equal T (lift h x1 x4)) (pr0_tau x3 x4 H7 x2)) t3
2013 H_x)))) (H2 x3 x1 H6)) x0 H4)))))) (lift_gen_flat Cast u t2 x0 h x1
2014 H3)))))))))) y x H0))))) H))))).
projects / helm.git / blob