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