1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "basic_1/pr0/defs.ma".
19 include "basic_1/subst0/fwd.ma".
21 implied rec lemma pr0_ind (P: (T \to (T \to Prop))) (f: (\forall (t: T).(P t
22 t))) (f0: (\forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to ((P u1 u2) \to
23 (\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to ((P t1 t2) \to (\forall
24 (k: K).(P (THead k u1 t1) (THead k u2 t2)))))))))))) (f1: (\forall (u:
25 T).(\forall (v1: T).(\forall (v2: T).((pr0 v1 v2) \to ((P v1 v2) \to (\forall
26 (t1: T).(\forall (t2: T).((pr0 t1 t2) \to ((P t1 t2) \to (P (THead (Flat
27 Appl) v1 (THead (Bind Abst) u t1)) (THead (Bind Abbr) v2 t2)))))))))))) (f2:
28 (\forall (b: B).((not (eq B b Abst)) \to (\forall (v1: T).(\forall (v2:
29 T).((pr0 v1 v2) \to ((P v1 v2) \to (\forall (u1: T).(\forall (u2: T).((pr0 u1
30 u2) \to ((P u1 u2) \to (\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to ((P
31 t1 t2) \to (P (THead (Flat Appl) v1 (THead (Bind b) u1 t1)) (THead (Bind b)
32 u2 (THead (Flat Appl) (lift (S O) O v2) t2)))))))))))))))))) (f3: (\forall
33 (u1: T).(\forall (u2: T).((pr0 u1 u2) \to ((P u1 u2) \to (\forall (t1:
34 T).(\forall (t2: T).((pr0 t1 t2) \to ((P t1 t2) \to (\forall (w: T).((subst0
35 O u2 t2 w) \to (P (THead (Bind Abbr) u1 t1) (THead (Bind Abbr) u2
36 w))))))))))))) (f4: (\forall (b: B).((not (eq B b Abst)) \to (\forall (t1:
37 T).(\forall (t2: T).((pr0 t1 t2) \to ((P t1 t2) \to (\forall (u: T).(P (THead
38 (Bind b) u (lift (S O) O t1)) t2))))))))) (f5: (\forall (t1: T).(\forall (t2:
39 T).((pr0 t1 t2) \to ((P t1 t2) \to (\forall (u: T).(P (THead (Flat Cast) u
40 t1) t2))))))) (t: T) (t0: T) (p: pr0 t t0) on p: P t t0 \def match p with
41 [(pr0_refl t1) \Rightarrow (f t1) | (pr0_comp u1 u2 p0 t1 t2 p1 k)
42 \Rightarrow (f0 u1 u2 p0 ((pr0_ind P f f0 f1 f2 f3 f4 f5) u1 u2 p0) t1 t2 p1
43 ((pr0_ind P f f0 f1 f2 f3 f4 f5) t1 t2 p1) k) | (pr0_beta u v1 v2 p0 t1 t2
44 p1) \Rightarrow (f1 u v1 v2 p0 ((pr0_ind P f f0 f1 f2 f3 f4 f5) v1 v2 p0) t1
45 t2 p1 ((pr0_ind P f f0 f1 f2 f3 f4 f5) t1 t2 p1)) | (pr0_upsilon b n v1 v2 p0
46 u1 u2 p1 t1 t2 p2) \Rightarrow (f2 b n v1 v2 p0 ((pr0_ind P f f0 f1 f2 f3 f4
47 f5) v1 v2 p0) u1 u2 p1 ((pr0_ind P f f0 f1 f2 f3 f4 f5) u1 u2 p1) t1 t2 p2
48 ((pr0_ind P f f0 f1 f2 f3 f4 f5) t1 t2 p2)) | (pr0_delta u1 u2 p0 t1 t2 p1 w
49 s0) \Rightarrow (f3 u1 u2 p0 ((pr0_ind P f f0 f1 f2 f3 f4 f5) u1 u2 p0) t1 t2
50 p1 ((pr0_ind P f f0 f1 f2 f3 f4 f5) t1 t2 p1) w s0) | (pr0_zeta b n t1 t2 p0
51 u) \Rightarrow (f4 b n t1 t2 p0 ((pr0_ind P f f0 f1 f2 f3 f4 f5) t1 t2 p0) u)
52 | (pr0_tau t1 t2 p0 u) \Rightarrow (f5 t1 t2 p0 ((pr0_ind P f f0 f1 f2 f3 f4
56 \forall (x: T).(\forall (n: nat).((pr0 (TSort n) x) \to (eq T x (TSort n))))
58 \lambda (x: T).(\lambda (n: nat).(\lambda (H: (pr0 (TSort n) x)).(insert_eq
59 T (TSort n) (\lambda (t: T).(pr0 t x)) (\lambda (t: T).(eq T x t)) (\lambda
60 (y: T).(\lambda (H0: (pr0 y x)).(pr0_ind (\lambda (t: T).(\lambda (t0:
61 T).((eq T t (TSort n)) \to (eq T t0 t)))) (\lambda (t: T).(\lambda (H1: (eq T
62 t (TSort n))).(let H2 \def (f_equal T T (\lambda (e: T).e) t (TSort n) H1) in
63 (eq_ind_r T (TSort n) (\lambda (t0: T).(eq T t0 t0)) (refl_equal T (TSort n))
64 t H2)))) (\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda
65 (_: (((eq T u1 (TSort n)) \to (eq T u2 u1)))).(\lambda (t1: T).(\lambda (t2:
66 T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq T t2
67 t1)))).(\lambda (k: K).(\lambda (H5: (eq T (THead k u1 t1) (TSort n))).(let
68 H6 \def (eq_ind T (THead k u1 t1) (\lambda (ee: T).(match ee with [(TSort _)
69 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
70 True])) I (TSort n) H5) in (False_ind (eq T (THead k u2 t2) (THead k u1 t1))
71 H6)))))))))))) (\lambda (u: T).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_:
72 (pr0 v1 v2)).(\lambda (_: (((eq T v1 (TSort n)) \to (eq T v2 v1)))).(\lambda
73 (t1: T).(\lambda (t2: T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1
74 (TSort n)) \to (eq T t2 t1)))).(\lambda (H5: (eq T (THead (Flat Appl) v1
75 (THead (Bind Abst) u t1)) (TSort n))).(let H6 \def (eq_ind T (THead (Flat
76 Appl) v1 (THead (Bind Abst) u t1)) (\lambda (ee: T).(match ee with [(TSort _)
77 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
78 True])) I (TSort n) H5) in (False_ind (eq T (THead (Bind Abbr) v2 t2) (THead
79 (Flat Appl) v1 (THead (Bind Abst) u t1))) H6)))))))))))) (\lambda (b:
80 B).(\lambda (_: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2:
81 T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 (TSort n)) \to (eq T v2
82 v1)))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda
83 (_: (((eq T u1 (TSort n)) \to (eq T u2 u1)))).(\lambda (t1: T).(\lambda (t2:
84 T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq T t2
85 t1)))).(\lambda (H8: (eq T (THead (Flat Appl) v1 (THead (Bind b) u1 t1))
86 (TSort n))).(let H9 \def (eq_ind T (THead (Flat Appl) v1 (THead (Bind b) u1
87 t1)) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
88 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H8) in
89 (False_ind (eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2))
90 (THead (Flat Appl) v1 (THead (Bind b) u1 t1))) H9))))))))))))))))) (\lambda
91 (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (_: (((eq T u1
92 (TSort n)) \to (eq T u2 u1)))).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_:
93 (pr0 t1 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq T t2 t1)))).(\lambda
94 (w: T).(\lambda (_: (subst0 O u2 t2 w)).(\lambda (H6: (eq T (THead (Bind
95 Abbr) u1 t1) (TSort n))).(let H7 \def (eq_ind T (THead (Bind Abbr) u1 t1)
96 (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
97 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H6) in
98 (False_ind (eq T (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u1 t1))
99 H7))))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda
100 (t1: T).(\lambda (t2: T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1
101 (TSort n)) \to (eq T t2 t1)))).(\lambda (u: T).(\lambda (H4: (eq T (THead
102 (Bind b) u (lift (S O) O t1)) (TSort n))).(let H5 \def (eq_ind T (THead (Bind
103 b) u (lift (S O) O t1)) (\lambda (ee: T).(match ee with [(TSort _)
104 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
105 True])) I (TSort n) H4) in (False_ind (eq T t2 (THead (Bind b) u (lift (S O)
106 O t1))) H5)))))))))) (\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (pr0 t1
107 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq T t2 t1)))).(\lambda (u:
108 T).(\lambda (H3: (eq T (THead (Flat Cast) u t1) (TSort n))).(let H4 \def
109 (eq_ind T (THead (Flat Cast) u t1) (\lambda (ee: T).(match ee with [(TSort _)
110 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
111 True])) I (TSort n) H3) in (False_ind (eq T t2 (THead (Flat Cast) u t1))
112 H4)))))))) y x H0))) H))).
115 \forall (x: T).(\forall (n: nat).((pr0 (TLRef n) x) \to (eq T x (TLRef n))))
117 \lambda (x: T).(\lambda (n: nat).(\lambda (H: (pr0 (TLRef n) x)).(insert_eq
118 T (TLRef n) (\lambda (t: T).(pr0 t x)) (\lambda (t: T).(eq T x t)) (\lambda
119 (y: T).(\lambda (H0: (pr0 y x)).(pr0_ind (\lambda (t: T).(\lambda (t0:
120 T).((eq T t (TLRef n)) \to (eq T t0 t)))) (\lambda (t: T).(\lambda (H1: (eq T
121 t (TLRef n))).(let H2 \def (f_equal T T (\lambda (e: T).e) t (TLRef n) H1) in
122 (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T t0 t0)) (refl_equal T (TLRef n))
123 t H2)))) (\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda
124 (_: (((eq T u1 (TLRef n)) \to (eq T u2 u1)))).(\lambda (t1: T).(\lambda (t2:
125 T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1 (TLRef n)) \to (eq T t2
126 t1)))).(\lambda (k: K).(\lambda (H5: (eq T (THead k u1 t1) (TLRef n))).(let
127 H6 \def (eq_ind T (THead k u1 t1) (\lambda (ee: T).(match ee with [(TSort _)
128 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
129 True])) I (TLRef n) H5) in (False_ind (eq T (THead k u2 t2) (THead k u1 t1))
130 H6)))))))))))) (\lambda (u: T).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_:
131 (pr0 v1 v2)).(\lambda (_: (((eq T v1 (TLRef n)) \to (eq T v2 v1)))).(\lambda
132 (t1: T).(\lambda (t2: T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1
133 (TLRef n)) \to (eq T t2 t1)))).(\lambda (H5: (eq T (THead (Flat Appl) v1
134 (THead (Bind Abst) u t1)) (TLRef n))).(let H6 \def (eq_ind T (THead (Flat
135 Appl) v1 (THead (Bind Abst) u t1)) (\lambda (ee: T).(match ee with [(TSort _)
136 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
137 True])) I (TLRef n) H5) in (False_ind (eq T (THead (Bind Abbr) v2 t2) (THead
138 (Flat Appl) v1 (THead (Bind Abst) u t1))) H6)))))))))))) (\lambda (b:
139 B).(\lambda (_: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2:
140 T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 (TLRef n)) \to (eq T v2
141 v1)))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda
142 (_: (((eq T u1 (TLRef n)) \to (eq T u2 u1)))).(\lambda (t1: T).(\lambda (t2:
143 T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1 (TLRef n)) \to (eq T t2
144 t1)))).(\lambda (H8: (eq T (THead (Flat Appl) v1 (THead (Bind b) u1 t1))
145 (TLRef n))).(let H9 \def (eq_ind T (THead (Flat Appl) v1 (THead (Bind b) u1
146 t1)) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
147 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H8) in
148 (False_ind (eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2))
149 (THead (Flat Appl) v1 (THead (Bind b) u1 t1))) H9))))))))))))))))) (\lambda
150 (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (_: (((eq T u1
151 (TLRef n)) \to (eq T u2 u1)))).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_:
152 (pr0 t1 t2)).(\lambda (_: (((eq T t1 (TLRef n)) \to (eq T t2 t1)))).(\lambda
153 (w: T).(\lambda (_: (subst0 O u2 t2 w)).(\lambda (H6: (eq T (THead (Bind
154 Abbr) u1 t1) (TLRef n))).(let H7 \def (eq_ind T (THead (Bind Abbr) u1 t1)
155 (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
156 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H6) in
157 (False_ind (eq T (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u1 t1))
158 H7))))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda
159 (t1: T).(\lambda (t2: T).(\lambda (_: (pr0 t1 t2)).(\lambda (_: (((eq T t1
160 (TLRef n)) \to (eq T t2 t1)))).(\lambda (u: T).(\lambda (H4: (eq T (THead
161 (Bind b) u (lift (S O) O t1)) (TLRef n))).(let H5 \def (eq_ind T (THead (Bind
162 b) u (lift (S O) O t1)) (\lambda (ee: T).(match ee with [(TSort _)
163 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
164 True])) I (TLRef n) H4) in (False_ind (eq T t2 (THead (Bind b) u (lift (S O)
165 O t1))) H5)))))))))) (\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (pr0 t1
166 t2)).(\lambda (_: (((eq T t1 (TLRef n)) \to (eq T t2 t1)))).(\lambda (u:
167 T).(\lambda (H3: (eq T (THead (Flat Cast) u t1) (TLRef n))).(let H4 \def
168 (eq_ind T (THead (Flat Cast) u t1) (\lambda (ee: T).(match ee with [(TSort _)
169 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
170 True])) I (TLRef n) H3) in (False_ind (eq T t2 (THead (Flat Cast) u t1))
171 H4)))))))) y x H0))) H))).
174 \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Bind Abst) u1
175 t1) x) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Bind
176 Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
177 T).(\lambda (t2: T).(pr0 t1 t2)))))))
179 \lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (H: (pr0 (THead
180 (Bind Abst) u1 t1) x)).(insert_eq T (THead (Bind Abst) u1 t1) (\lambda (t:
181 T).(pr0 t x)) (\lambda (_: T).(ex3_2 T T (\lambda (u2: T).(\lambda (t2:
182 T).(eq T x (THead (Bind Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0
183 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2))))) (\lambda (y:
184 T).(\lambda (H0: (pr0 y x)).(pr0_ind (\lambda (t: T).(\lambda (t0: T).((eq T
185 t (THead (Bind Abst) u1 t1)) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
186 T).(eq T t0 (THead (Bind Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_:
187 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2))))))) (\lambda
188 (t: T).(\lambda (H1: (eq T t (THead (Bind Abst) u1 t1))).(let H2 \def
189 (f_equal T T (\lambda (e: T).e) t (THead (Bind Abst) u1 t1) H1) in (eq_ind_r
190 T (THead (Bind Abst) u1 t1) (\lambda (t0: T).(ex3_2 T T (\lambda (u2:
191 T).(\lambda (t2: T).(eq T t0 (THead (Bind Abst) u2 t2)))) (\lambda (u2:
192 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1
193 t2))))) (ex3_2_intro T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Bind
194 Abst) u1 t1) (THead (Bind Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_:
195 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2))) u1 t1
196 (refl_equal T (THead (Bind Abst) u1 t1)) (pr0_refl u1) (pr0_refl t1)) t
197 H2)))) (\lambda (u0: T).(\lambda (u2: T).(\lambda (H1: (pr0 u0 u2)).(\lambda
198 (H2: (((eq T u0 (THead (Bind Abst) u1 t1)) \to (ex3_2 T T (\lambda (u3:
199 T).(\lambda (t2: T).(eq T u2 (THead (Bind Abst) u3 t2)))) (\lambda (u3:
200 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1
201 t2))))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H3: (pr0 t0
202 t2)).(\lambda (H4: (((eq T t0 (THead (Bind Abst) u1 t1)) \to (ex3_2 T T
203 (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst) u3 t3))))
204 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
205 T).(pr0 t1 t3))))))).(\lambda (k: K).(\lambda (H5: (eq T (THead k u0 t0)
206 (THead (Bind Abst) u1 t1))).(let H6 \def (f_equal T K (\lambda (e: T).(match
207 e with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _)
208 \Rightarrow k0])) (THead k u0 t0) (THead (Bind Abst) u1 t1) H5) in ((let H7
209 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow u0 |
210 (TLRef _) \Rightarrow u0 | (THead _ t _) \Rightarrow t])) (THead k u0 t0)
211 (THead (Bind Abst) u1 t1) H5) in ((let H8 \def (f_equal T T (\lambda (e:
212 T).(match e with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 |
213 (THead _ _ t) \Rightarrow t])) (THead k u0 t0) (THead (Bind Abst) u1 t1) H5)
214 in (\lambda (H9: (eq T u0 u1)).(\lambda (H10: (eq K k (Bind Abst))).(eq_ind_r
215 K (Bind Abst) (\lambda (k0: K).(ex3_2 T T (\lambda (u3: T).(\lambda (t3:
216 T).(eq T (THead k0 u2 t2) (THead (Bind Abst) u3 t3)))) (\lambda (u3:
217 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
218 t3))))) (let H11 \def (eq_ind T t0 (\lambda (t: T).((eq T t (THead (Bind
219 Abst) u1 t1)) \to (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2
220 (THead (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3)))
221 (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))))) H4 t1 H8) in (let H12 \def
222 (eq_ind T t0 (\lambda (t: T).(pr0 t t2)) H3 t1 H8) in (let H13 \def (eq_ind T
223 u0 (\lambda (t: T).((eq T t (THead (Bind Abst) u1 t1)) \to (ex3_2 T T
224 (\lambda (u3: T).(\lambda (t3: T).(eq T u2 (THead (Bind Abst) u3 t3))))
225 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
226 T).(pr0 t1 t3)))))) H2 u1 H9) in (let H14 \def (eq_ind T u0 (\lambda (t:
227 T).(pr0 t u2)) H1 u1 H9) in (ex3_2_intro T T (\lambda (u3: T).(\lambda (t3:
228 T).(eq T (THead (Bind Abst) u2 t2) (THead (Bind Abst) u3 t3)))) (\lambda (u3:
229 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
230 t3))) u2 t2 (refl_equal T (THead (Bind Abst) u2 t2)) H14 H12))))) k H10))))
231 H7)) H6)))))))))))) (\lambda (u: T).(\lambda (v1: T).(\lambda (v2:
232 T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind Abst) u1
233 t1)) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Bind
234 Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
235 T).(\lambda (t2: T).(pr0 t1 t2))))))).(\lambda (t0: T).(\lambda (t2:
236 T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind Abst) u1
237 t1)) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
238 Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
239 T).(\lambda (t3: T).(pr0 t1 t3))))))).(\lambda (H5: (eq T (THead (Flat Appl)
240 v1 (THead (Bind Abst) u t0)) (THead (Bind Abst) u1 t1))).(let H6 \def (eq_ind
241 T (THead (Flat Appl) v1 (THead (Bind Abst) u t0)) (\lambda (ee: T).(match ee
242 with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _
243 _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat _)
244 \Rightarrow True])])) I (THead (Bind Abst) u1 t1) H5) in (False_ind (ex3_2 T
245 T (\lambda (u2: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) v2 t2) (THead
246 (Bind Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
247 (_: T).(\lambda (t3: T).(pr0 t1 t3)))) H6)))))))))))) (\lambda (b:
248 B).(\lambda (_: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2:
249 T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind Abst) u1
250 t1)) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Bind
251 Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
252 T).(\lambda (t2: T).(pr0 t1 t2))))))).(\lambda (u0: T).(\lambda (u2:
253 T).(\lambda (_: (pr0 u0 u2)).(\lambda (_: (((eq T u0 (THead (Bind Abst) u1
254 t1)) \to (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead (Bind
255 Abst) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
256 T).(\lambda (t2: T).(pr0 t1 t2))))))).(\lambda (t0: T).(\lambda (t2:
257 T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind Abst) u1
258 t1)) \to (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind
259 Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
260 T).(\lambda (t3: T).(pr0 t1 t3))))))).(\lambda (H8: (eq T (THead (Flat Appl)
261 v1 (THead (Bind b) u0 t0)) (THead (Bind Abst) u1 t1))).(let H9 \def (eq_ind T
262 (THead (Flat Appl) v1 (THead (Bind b) u0 t0)) (\lambda (ee: T).(match ee with
263 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
264 \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
265 True])])) I (THead (Bind Abst) u1 t1) H8) in (False_ind (ex3_2 T T (\lambda
266 (u3: T).(\lambda (t3: T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S
267 O) O v2) t2)) (THead (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_:
268 T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3))))
269 H9))))))))))))))))) (\lambda (u0: T).(\lambda (u2: T).(\lambda (_: (pr0 u0
270 u2)).(\lambda (_: (((eq T u0 (THead (Bind Abst) u1 t1)) \to (ex3_2 T T
271 (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead (Bind Abst) u3 t2))))
272 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t2:
273 T).(pr0 t1 t2))))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0
274 t2)).(\lambda (_: (((eq T t0 (THead (Bind Abst) u1 t1)) \to (ex3_2 T T
275 (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst) u3 t3))))
276 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
277 T).(pr0 t1 t3))))))).(\lambda (w: T).(\lambda (_: (subst0 O u2 t2
278 w)).(\lambda (H6: (eq T (THead (Bind Abbr) u0 t0) (THead (Bind Abst) u1
279 t1))).(let H7 \def (eq_ind T (THead (Bind Abbr) u0 t0) (\lambda (ee:
280 T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
281 | (THead k _ _) \Rightarrow (match k with [(Bind b) \Rightarrow (match b with
282 [Abbr \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow False]) |
283 (Flat _) \Rightarrow False])])) I (THead (Bind Abst) u1 t1) H6) in (False_ind
284 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) u2 w)
285 (THead (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3)))
286 (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) H7))))))))))))) (\lambda (b:
287 B).(\lambda (H1: (not (eq B b Abst))).(\lambda (t0: T).(\lambda (t2:
288 T).(\lambda (_: (pr0 t0 t2)).(\lambda (H3: (((eq T t0 (THead (Bind Abst) u1
289 t1)) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
290 Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
291 T).(\lambda (t3: T).(pr0 t1 t3))))))).(\lambda (u: T).(\lambda (H4: (eq T
292 (THead (Bind b) u (lift (S O) O t0)) (THead (Bind Abst) u1 t1))).(let H5 \def
293 (f_equal T B (\lambda (e: T).(match e with [(TSort _) \Rightarrow b | (TLRef
294 _) \Rightarrow b | (THead k _ _) \Rightarrow (match k with [(Bind b0)
295 \Rightarrow b0 | (Flat _) \Rightarrow b])])) (THead (Bind b) u (lift (S O) O
296 t0)) (THead (Bind Abst) u1 t1) H4) in ((let H6 \def (f_equal T T (\lambda (e:
297 T).(match e with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | (THead
298 _ t _) \Rightarrow t])) (THead (Bind b) u (lift (S O) O t0)) (THead (Bind
299 Abst) u1 t1) H4) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e with
300 [(TSort _) \Rightarrow (lref_map (\lambda (x0: nat).(plus x0 (S O))) O t0) |
301 (TLRef _) \Rightarrow (lref_map (\lambda (x0: nat).(plus x0 (S O))) O t0) |
302 (THead _ _ t) \Rightarrow t])) (THead (Bind b) u (lift (S O) O t0)) (THead
303 (Bind Abst) u1 t1) H4) in (\lambda (_: (eq T u u1)).(\lambda (H9: (eq B b
304 Abst)).(let H10 \def (eq_ind B b (\lambda (b0: B).(not (eq B b0 Abst))) H1
305 Abst H9) in (let H11 \def (eq_ind_r T t1 (\lambda (t: T).((eq T t0 (THead
306 (Bind Abst) u1 t)) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2
307 (THead (Bind Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))
308 (\lambda (_: T).(\lambda (t3: T).(pr0 t t3)))))) H3 (lift (S O) O t0) H7) in
309 (eq_ind T (lift (S O) O t0) (\lambda (t: T).(ex3_2 T T (\lambda (u2:
310 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst) u2 t3)))) (\lambda (u2:
311 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t
312 t3))))) (let H12 \def (match (H10 (refl_equal B Abst)) in False with []) in
313 H12) t1 H7)))))) H6)) H5)))))))))) (\lambda (t0: T).(\lambda (t2: T).(\lambda
314 (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind Abst) u1 t1)) \to
315 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst) u2
316 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
317 T).(\lambda (t3: T).(pr0 t1 t3))))))).(\lambda (u: T).(\lambda (H3: (eq T
318 (THead (Flat Cast) u t0) (THead (Bind Abst) u1 t1))).(let H4 \def (eq_ind T
319 (THead (Flat Cast) u t0) (\lambda (ee: T).(match ee with [(TSort _)
320 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
321 (match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I
322 (THead (Bind Abst) u1 t1) H3) in (False_ind (ex3_2 T T (\lambda (u2:
323 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst) u2 t3)))) (\lambda (u2:
324 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
325 t3)))) H4)))))))) y x H0))) H)))).
328 \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Flat Appl) u1
329 t1) x) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead
330 (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
331 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1:
332 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
333 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
334 (t2: T).(eq T x (THead (Bind Abbr) u2 t2)))))) (\lambda (_: T).(\lambda (_:
335 T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
336 (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))) (ex6_6 B T T T T T
337 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
338 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
339 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
340 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
341 T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t2: T).(eq T x (THead (Bind b)
342 v2 (THead (Flat Appl) (lift (S O) O u2) t2))))))))) (\lambda (_: B).(\lambda
343 (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0
344 u1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
345 T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_:
346 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
347 (t2: T).(pr0 z1 t2))))))))))))
349 \lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (H: (pr0 (THead
350 (Flat Appl) u1 t1) x)).(insert_eq T (THead (Flat Appl) u1 t1) (\lambda (t:
351 T).(pr0 t x)) (\lambda (_: T).(or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
352 T).(eq T x (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0
353 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T
354 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
355 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
356 T).(\lambda (t2: T).(eq T x (THead (Bind Abbr) u2 t2)))))) (\lambda (_:
357 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda
358 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2))))))
359 (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
360 (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
361 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
362 (_: T).(eq T t1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
363 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t2: T).(eq T x
364 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2))))))))) (\lambda
365 (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
366 T).(\lambda (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda (y1:
367 T).(\lambda (_: T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1
368 v2))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_:
369 T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))))))) (\lambda (y:
370 T).(\lambda (H0: (pr0 y x)).(pr0_ind (\lambda (t: T).(\lambda (t0: T).((eq T
371 t (THead (Flat Appl) u1 t1)) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda
372 (t2: T).(eq T t0 (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_:
373 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T
374 T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
375 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
376 T).(\lambda (t2: T).(eq T t0 (THead (Bind Abbr) u2 t2)))))) (\lambda (_:
377 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda
378 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2))))))
379 (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
380 (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
381 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
382 (_: T).(eq T t1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
383 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t2: T).(eq T
384 t0 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2)))))))))
385 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
386 T).(\lambda (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda (y1:
387 T).(\lambda (_: T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1
388 v2))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_:
389 T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))))))))) (\lambda (t:
390 T).(\lambda (H1: (eq T t (THead (Flat Appl) u1 t1))).(let H2 \def (f_equal T
391 T (\lambda (e: T).e) t (THead (Flat Appl) u1 t1) H1) in (eq_ind_r T (THead
392 (Flat Appl) u1 t1) (\lambda (t0: T).(or3 (ex3_2 T T (\lambda (u2: T).(\lambda
393 (t2: T).(eq T t0 (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_:
394 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T
395 T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
396 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
397 T).(\lambda (t2: T).(eq T t0 (THead (Bind Abbr) u2 t2)))))) (\lambda (_:
398 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda
399 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2))))))
400 (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
401 (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
402 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
403 (_: T).(eq T t1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
404 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t2: T).(eq T
405 t0 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t2)))))))))
406 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
407 T).(\lambda (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda (y1:
408 T).(\lambda (_: T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1
409 v2))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_:
410 T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))))))) (or3_intro0 (ex3_2 T
411 T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Flat Appl) u1 t1) (THead
412 (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
413 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1:
414 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
415 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
416 (t2: T).(eq T (THead (Flat Appl) u1 t1) (THead (Bind Abbr) u2 t2))))))
417 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1
418 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2:
419 T).(pr0 z1 t2)))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_:
420 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
421 b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
422 T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind b) y1 z1))))))))
423 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
424 (v2: T).(\lambda (t2: T).(eq T (THead (Flat Appl) u1 t1) (THead (Bind b) v2
425 (THead (Flat Appl) (lift (S O) O u2) t2))))))))) (\lambda (_: B).(\lambda (_:
426 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
427 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
428 T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_:
429 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
430 (t2: T).(pr0 z1 t2)))))))) (ex3_2_intro T T (\lambda (u2: T).(\lambda (t2:
431 T).(eq T (THead (Flat Appl) u1 t1) (THead (Flat Appl) u2 t2)))) (\lambda (u2:
432 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1
433 t2))) u1 t1 (refl_equal T (THead (Flat Appl) u1 t1)) (pr0_refl u1) (pr0_refl
434 t1))) t H2)))) (\lambda (u0: T).(\lambda (u2: T).(\lambda (H1: (pr0 u0
435 u2)).(\lambda (H2: (((eq T u0 (THead (Flat Appl) u1 t1)) \to (or3 (ex3_2 T T
436 (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead (Flat Appl) u3 t2))))
437 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t2:
438 T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
439 (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
440 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead (Bind
441 Abbr) u3 t2)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
442 (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
443 T).(\lambda (t2: T).(pr0 z1 t2)))))) (ex6_6 B T T T T T (\lambda (b:
444 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
445 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
446 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
447 b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
448 (u3: T).(\lambda (v2: T).(\lambda (t2: T).(eq T u2 (THead (Bind b) v2 (THead
449 (Flat Appl) (lift (S O) O u3) t2))))))))) (\lambda (_: B).(\lambda (_:
450 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
451 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
452 T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_:
453 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
454 (t2: T).(pr0 z1 t2)))))))))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda
455 (H3: (pr0 t0 t2)).(\lambda (H4: (((eq T t0 (THead (Flat Appl) u1 t1)) \to
456 (or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl)
457 u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
458 T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
459 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1
460 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3:
461 T).(eq T t2 (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_:
462 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
463 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
464 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
465 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
466 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
467 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
468 T).(\lambda (u3: T).(\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
469 b) v2 (THead (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_:
470 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
471 (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
472 T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2)))))))
473 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
474 T).(\lambda (t3: T).(pr0 z1 t3)))))))))))).(\lambda (k: K).(\lambda (H5: (eq
475 T (THead k u0 t0) (THead (Flat Appl) u1 t1))).(let H6 \def (f_equal T K
476 (\lambda (e: T).(match e with [(TSort _) \Rightarrow k | (TLRef _)
477 \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k u0 t0) (THead (Flat
478 Appl) u1 t1) H5) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e with
479 [(TSort _) \Rightarrow u0 | (TLRef _) \Rightarrow u0 | (THead _ t _)
480 \Rightarrow t])) (THead k u0 t0) (THead (Flat Appl) u1 t1) H5) in ((let H8
481 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow t0 |
482 (TLRef _) \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead k u0 t0)
483 (THead (Flat Appl) u1 t1) H5) in (\lambda (H9: (eq T u0 u1)).(\lambda (H10:
484 (eq K k (Flat Appl))).(eq_ind_r K (Flat Appl) (\lambda (k0: K).(or3 (ex3_2 T
485 T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead k0 u2 t2) (THead (Flat Appl)
486 u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
487 T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
488 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1
489 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3:
490 T).(eq T (THead k0 u2 t2) (THead (Bind Abbr) u3 t3)))))) (\lambda (_:
491 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda
492 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3))))))
493 (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
494 (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
495 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
496 (_: T).(eq T t1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
497 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (v2: T).(\lambda (t3: T).(eq T
498 (THead k0 u2 t2) (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3)
499 t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3:
500 T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda
501 (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0
502 y1 v2))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_:
503 T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))))))) (let H11 \def
504 (eq_ind T t0 (\lambda (t: T).((eq T t (THead (Flat Appl) u1 t1)) \to (or3
505 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u3
506 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
507 T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
508 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1
509 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3:
510 T).(eq T t2 (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_:
511 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
512 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
513 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
514 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
515 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
516 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
517 T).(\lambda (u3: T).(\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
518 b) v2 (THead (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_:
519 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
520 (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
521 T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2)))))))
522 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
523 T).(\lambda (t3: T).(pr0 z1 t3))))))))))) H4 t1 H8) in (let H12 \def (eq_ind
524 T t0 (\lambda (t: T).(pr0 t t2)) H3 t1 H8) in (let H13 \def (eq_ind T u0
525 (\lambda (t: T).((eq T t (THead (Flat Appl) u1 t1)) \to (or3 (ex3_2 T T
526 (\lambda (u3: T).(\lambda (t3: T).(eq T u2 (THead (Flat Appl) u3 t3))))
527 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
528 T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
529 (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
530 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3: T).(eq T u2 (THead (Bind
531 Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
532 (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
533 T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b:
534 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
535 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
536 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
537 b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
538 (u3: T).(\lambda (v2: T).(\lambda (t3: T).(eq T u2 (THead (Bind b) v2 (THead
539 (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_: B).(\lambda (_:
540 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
541 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
542 T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_:
543 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
544 (t3: T).(pr0 z1 t3))))))))))) H2 u1 H9) in (let H14 \def (eq_ind T u0
545 (\lambda (t: T).(pr0 t u2)) H1 u1 H9) in (or3_intro0 (ex3_2 T T (\lambda (u3:
546 T).(\lambda (t3: T).(eq T (THead (Flat Appl) u2 t2) (THead (Flat Appl) u3
547 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
548 T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
549 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1
550 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3:
551 T).(eq T (THead (Flat Appl) u2 t2) (THead (Bind Abbr) u3 t3)))))) (\lambda
552 (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3)))))
553 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1
554 t3)))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_:
555 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst))))))))
556 (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
557 (_: T).(\lambda (_: T).(eq T t1 (THead (Bind b) y1 z1)))))))) (\lambda (b:
558 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (v2: T).(\lambda
559 (t3: T).(eq T (THead (Flat Appl) u2 t2) (THead (Bind b) v2 (THead (Flat Appl)
560 (lift (S O) O u3) t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_:
561 T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u3)))))))
562 (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
563 (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_: B).(\lambda (_:
564 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1
565 t3)))))))) (ex3_2_intro T T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead
566 (Flat Appl) u2 t2) (THead (Flat Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_:
567 T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3))) u2 t2
568 (refl_equal T (THead (Flat Appl) u2 t2)) H14 H12)))))) k H10)))) H7))
569 H6)))))))))))) (\lambda (u: T).(\lambda (v1: T).(\lambda (v2: T).(\lambda
570 (H1: (pr0 v1 v2)).(\lambda (H2: (((eq T v1 (THead (Flat Appl) u1 t1)) \to
571 (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Flat Appl)
572 u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
573 T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
574 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1
575 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t2:
576 T).(eq T v2 (THead (Bind Abbr) u2 t2)))))) (\lambda (_: T).(\lambda (_:
577 T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
578 (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))) (ex6_6 B T T T T T
579 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
580 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
581 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
582 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
583 T).(\lambda (u2: T).(\lambda (v3: T).(\lambda (t2: T).(eq T v2 (THead (Bind
584 b) v3 (THead (Flat Appl) (lift (S O) O u2) t2))))))))) (\lambda (_:
585 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda
586 (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
587 T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3)))))))
588 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
589 T).(\lambda (t2: T).(pr0 z1 t2)))))))))))).(\lambda (t0: T).(\lambda (t2:
590 T).(\lambda (H3: (pr0 t0 t2)).(\lambda (H4: (((eq T t0 (THead (Flat Appl) u1
591 t1)) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead
592 (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
593 (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1:
594 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
595 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
596 (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
597 T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
598 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
599 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
600 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
601 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
602 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
603 T).(\lambda (u2: T).(\lambda (v3: T).(\lambda (t3: T).(eq T t2 (THead (Bind
604 b) v3 (THead (Flat Appl) (lift (S O) O u2) t3))))))))) (\lambda (_:
605 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda
606 (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
607 T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3)))))))
608 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
609 T).(\lambda (t3: T).(pr0 z1 t3)))))))))))).(\lambda (H5: (eq T (THead (Flat
610 Appl) v1 (THead (Bind Abst) u t0)) (THead (Flat Appl) u1 t1))).(let H6 \def
611 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow v1 | (TLRef
612 _) \Rightarrow v1 | (THead _ t _) \Rightarrow t])) (THead (Flat Appl) v1
613 (THead (Bind Abst) u t0)) (THead (Flat Appl) u1 t1) H5) in ((let H7 \def
614 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow (THead
615 (Bind Abst) u t0) | (TLRef _) \Rightarrow (THead (Bind Abst) u t0) | (THead _
616 _ t) \Rightarrow t])) (THead (Flat Appl) v1 (THead (Bind Abst) u t0)) (THead
617 (Flat Appl) u1 t1) H5) in (\lambda (H8: (eq T v1 u1)).(let H9 \def (eq_ind T
618 v1 (\lambda (t: T).((eq T t (THead (Flat Appl) u1 t1)) \to (or3 (ex3_2 T T
619 (\lambda (u2: T).(\lambda (t3: T).(eq T v2 (THead (Flat Appl) u2 t3))))
620 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
621 T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
622 (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
623 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T v2 (THead (Bind
624 Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
625 (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
626 T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b:
627 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
628 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
629 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
630 b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
631 (u2: T).(\lambda (v3: T).(\lambda (t3: T).(eq T v2 (THead (Bind b) v3 (THead
632 (Flat Appl) (lift (S O) O u2) t3))))))))) (\lambda (_: B).(\lambda (_:
633 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
634 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
635 T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_:
636 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
637 (t3: T).(pr0 z1 t3))))))))))) H2 u1 H8) in (let H10 \def (eq_ind T v1
638 (\lambda (t: T).(pr0 t v2)) H1 u1 H8) in (let H11 \def (eq_ind_r T t1
639 (\lambda (t: T).((eq T t0 (THead (Flat Appl) u1 t)) \to (or3 (ex3_2 T T
640 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3))))
641 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
642 T).(pr0 t t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
643 (_: T).(\lambda (_: T).(eq T t (THead (Bind Abst) y1 z1)))))) (\lambda (_:
644 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
645 Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
646 (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
647 T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b:
648 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
649 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
650 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t (THead (Bind
651 b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
652 (u2: T).(\lambda (v3: T).(\lambda (t3: T).(eq T t2 (THead (Bind b) v3 (THead
653 (Flat Appl) (lift (S O) O u2) t3))))))))) (\lambda (_: B).(\lambda (_:
654 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
655 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
656 T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_:
657 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
658 (t3: T).(pr0 z1 t3))))))))))) H4 (THead (Bind Abst) u t0) H7) in (let H12
659 \def (eq_ind_r T t1 (\lambda (t: T).((eq T u1 (THead (Flat Appl) u1 t)) \to
660 (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T v2 (THead (Flat Appl)
661 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
662 T).(\lambda (t3: T).(pr0 t t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
663 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t (THead (Bind Abst) y1
664 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3:
665 T).(eq T v2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
666 T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
667 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
668 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
669 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
670 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t
671 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
672 T).(\lambda (u2: T).(\lambda (v3: T).(\lambda (t3: T).(eq T v2 (THead (Bind
673 b) v3 (THead (Flat Appl) (lift (S O) O u2) t3))))))))) (\lambda (_:
674 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda
675 (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
676 T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3)))))))
677 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
678 T).(\lambda (t3: T).(pr0 z1 t3))))))))))) H9 (THead (Bind Abst) u t0) H7) in
679 (eq_ind T (THead (Bind Abst) u t0) (\lambda (t: T).(or3 (ex3_2 T T (\lambda
680 (u2: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) v2 t2) (THead (Flat Appl)
681 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
682 T).(\lambda (t3: T).(pr0 t t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
683 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t (THead (Bind Abst) y1
684 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3:
685 T).(eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abbr) u2 t3)))))) (\lambda
686 (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2)))))
687 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1
688 t3)))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_:
689 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst))))))))
690 (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
691 (_: T).(\lambda (_: T).(eq T t (THead (Bind b) y1 z1)))))))) (\lambda (b:
692 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (v3: T).(\lambda
693 (t3: T).(eq T (THead (Bind Abbr) v2 t2) (THead (Bind b) v3 (THead (Flat Appl)
694 (lift (S O) O u2) t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_:
695 T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u2)))))))
696 (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
697 (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_: B).(\lambda (_:
698 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1
699 t3)))))))))) (or3_intro1 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T
700 (THead (Bind Abbr) v2 t2) (THead (Flat Appl) u2 t3)))) (\lambda (u2:
701 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 (THead
702 (Bind Abst) u t0) t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1:
703 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind Abst) u t0) (THead
704 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
705 T).(\lambda (t3: T).(eq T (THead (Bind Abbr) v2 t2) (THead (Bind Abbr) u2
706 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
707 T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
708 (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_:
709 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
710 b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
711 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind Abst) u t0) (THead
712 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
713 T).(\lambda (u2: T).(\lambda (v3: T).(\lambda (t3: T).(eq T (THead (Bind
714 Abbr) v2 t2) (THead (Bind b) v3 (THead (Flat Appl) (lift (S O) O u2)
715 t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
716 T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda
717 (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0
718 y1 v3))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_:
719 T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))))) (ex4_4_intro T T T T
720 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
721 (THead (Bind Abst) u t0) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
722 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T (THead (Bind Abbr)
723 v2 t2) (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
724 T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
725 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3))))) u t0 v2 t2
726 (refl_equal T (THead (Bind Abst) u t0)) (refl_equal T (THead (Bind Abbr) v2
727 t2)) H10 H3)) t1 H7))))))) H6)))))))))))) (\lambda (b: B).(\lambda (H1: (not
728 (eq B b Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (H2: (pr0 v1
729 v2)).(\lambda (H3: (((eq T v1 (THead (Flat Appl) u1 t1)) \to (or3 (ex3_2 T T
730 (\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Flat Appl) u2 t2))))
731 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2:
732 T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
733 (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
734 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Bind
735 Abbr) u2 t2)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
736 (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
737 T).(\lambda (t2: T).(pr0 z1 t2)))))) (ex6_6 B T T T T T (\lambda (b0:
738 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
739 (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda
740 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
741 b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda
742 (u2: T).(\lambda (v3: T).(\lambda (t2: T).(eq T v2 (THead (Bind b0) v3 (THead
743 (Flat Appl) (lift (S O) O u2) t2))))))))) (\lambda (_: B).(\lambda (_:
744 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
745 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
746 T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_:
747 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
748 (t2: T).(pr0 z1 t2)))))))))))).(\lambda (u0: T).(\lambda (u2: T).(\lambda
749 (H4: (pr0 u0 u2)).(\lambda (H5: (((eq T u0 (THead (Flat Appl) u1 t1)) \to
750 (or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead (Flat Appl)
751 u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
752 T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
753 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1
754 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t2:
755 T).(eq T u2 (THead (Bind Abbr) u3 t2)))))) (\lambda (_: T).(\lambda (_:
756 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
757 (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))) (ex6_6 B T T T T T
758 (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
759 T).(\lambda (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1:
760 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
761 (THead (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
762 T).(\lambda (u3: T).(\lambda (v3: T).(\lambda (t2: T).(eq T u2 (THead (Bind
763 b0) v3 (THead (Flat Appl) (lift (S O) O u3) t2))))))))) (\lambda (_:
764 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
765 (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
766 T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3)))))))
767 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
768 T).(\lambda (t2: T).(pr0 z1 t2)))))))))))).(\lambda (t0: T).(\lambda (t2:
769 T).(\lambda (H6: (pr0 t0 t2)).(\lambda (H7: (((eq T t0 (THead (Flat Appl) u1
770 t1)) \to (or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead
771 (Flat Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
772 (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1:
773 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
774 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
775 (t3: T).(eq T t2 (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_:
776 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
777 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
778 (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
779 T).(\lambda (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1:
780 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
781 (THead (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
782 T).(\lambda (u3: T).(\lambda (v3: T).(\lambda (t3: T).(eq T t2 (THead (Bind
783 b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_:
784 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
785 (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
786 T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3)))))))
787 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
788 T).(\lambda (t3: T).(pr0 z1 t3)))))))))))).(\lambda (H8: (eq T (THead (Flat
789 Appl) v1 (THead (Bind b) u0 t0)) (THead (Flat Appl) u1 t1))).(let H9 \def
790 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow v1 | (TLRef
791 _) \Rightarrow v1 | (THead _ t _) \Rightarrow t])) (THead (Flat Appl) v1
792 (THead (Bind b) u0 t0)) (THead (Flat Appl) u1 t1) H8) in ((let H10 \def
793 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow (THead
794 (Bind b) u0 t0) | (TLRef _) \Rightarrow (THead (Bind b) u0 t0) | (THead _ _
795 t) \Rightarrow t])) (THead (Flat Appl) v1 (THead (Bind b) u0 t0)) (THead
796 (Flat Appl) u1 t1) H8) in (\lambda (H11: (eq T v1 u1)).(let H12 \def (eq_ind
797 T v1 (\lambda (t: T).((eq T t (THead (Flat Appl) u1 t1)) \to (or3 (ex3_2 T T
798 (\lambda (u3: T).(\lambda (t3: T).(eq T v2 (THead (Flat Appl) u3 t3))))
799 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
800 T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
801 (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
802 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3: T).(eq T v2 (THead (Bind
803 Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
804 (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
805 T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b0:
806 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
807 (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda
808 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
809 b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda
810 (u3: T).(\lambda (v3: T).(\lambda (t3: T).(eq T v2 (THead (Bind b0) v3 (THead
811 (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_: B).(\lambda (_:
812 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
813 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
814 T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_:
815 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
816 (t3: T).(pr0 z1 t3))))))))))) H3 u1 H11) in (let H13 \def (eq_ind T v1
817 (\lambda (t: T).(pr0 t v2)) H2 u1 H11) in (let H14 \def (eq_ind_r T t1
818 (\lambda (t: T).((eq T t0 (THead (Flat Appl) u1 t)) \to (or3 (ex3_2 T T
819 (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u3 t3))))
820 (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3:
821 T).(pr0 t t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
822 (_: T).(\lambda (_: T).(eq T t (THead (Bind Abst) y1 z1)))))) (\lambda (_:
823 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind
824 Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
825 (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
826 T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b0:
827 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
828 (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda
829 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t (THead (Bind
830 b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda
831 (u3: T).(\lambda (v3: T).(\lambda (t3: T).(eq T t2 (THead (Bind b0) v3 (THead
832 (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_: B).(\lambda (_:
833 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
834 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
835 T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_:
836 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
837 (t3: T).(pr0 z1 t3))))))))))) H7 (THead (Bind b) u0 t0) H10) in (let H15 \def
838 (eq_ind_r T t1 (\lambda (t: T).((eq T u0 (THead (Flat Appl) u1 t)) \to (or3
839 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T u2 (THead (Flat Appl) u3
840 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
841 T).(\lambda (t3: T).(pr0 t t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
842 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t (THead (Bind Abst) y1
843 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3:
844 T).(eq T u2 (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_:
845 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
846 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
847 (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
848 T).(\lambda (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1:
849 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t
850 (THead (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
851 T).(\lambda (u3: T).(\lambda (v3: T).(\lambda (t3: T).(eq T u2 (THead (Bind
852 b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_:
853 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
854 (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
855 T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3)))))))
856 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
857 T).(\lambda (t3: T).(pr0 z1 t3))))))))))) H5 (THead (Bind b) u0 t0) H10) in
858 (let H16 \def (eq_ind_r T t1 (\lambda (t: T).((eq T u1 (THead (Flat Appl) u1
859 t)) \to (or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T v2 (THead
860 (Flat Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
861 (_: T).(\lambda (t3: T).(pr0 t t3)))) (ex4_4 T T T T (\lambda (y1:
862 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t (THead (Bind
863 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
864 (t3: T).(eq T v2 (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_:
865 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
866 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
867 (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
868 T).(\lambda (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1:
869 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t
870 (THead (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
871 T).(\lambda (u3: T).(\lambda (v3: T).(\lambda (t3: T).(eq T v2 (THead (Bind
872 b0) v3 (THead (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_:
873 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
874 (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
875 T).(\lambda (_: T).(\lambda (v3: T).(\lambda (_: T).(pr0 y1 v3)))))))
876 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
877 T).(\lambda (t3: T).(pr0 z1 t3))))))))))) H12 (THead (Bind b) u0 t0) H10) in
878 (eq_ind T (THead (Bind b) u0 t0) (\lambda (t: T).(or3 (ex3_2 T T (\lambda
879 (u3: T).(\lambda (t3: T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S
880 O) O v2) t2)) (THead (Flat Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_:
881 T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t t3)))) (ex4_4 T T T
882 T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t
883 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3:
884 T).(\lambda (t3: T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O
885 v2) t2)) (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_:
886 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
887 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
888 (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
889 T).(\lambda (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1:
890 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t
891 (THead (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
892 T).(\lambda (u3: T).(\lambda (v3: T).(\lambda (t3: T).(eq T (THead (Bind b)
893 u2 (THead (Flat Appl) (lift (S O) O v2) t2)) (THead (Bind b0) v3 (THead (Flat
894 Appl) (lift (S O) O u3) t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda
895 (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u3)))))))
896 (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
897 (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_: B).(\lambda (_:
898 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1
899 t3)))))))))) (or3_intro2 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T
900 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)) (THead (Flat
901 Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
902 T).(\lambda (t3: T).(pr0 (THead (Bind b) u0 t0) t3)))) (ex4_4 T T T T
903 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
904 (THead (Bind b) u0 t0) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
905 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind b) u2
906 (THead (Flat Appl) (lift (S O) O v2) t2)) (THead (Bind Abbr) u3 t3))))))
907 (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1
908 u3))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3:
909 T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b0: B).(\lambda (_:
910 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
911 b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda
912 (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind b) u0 t0) (THead
913 (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
914 T).(\lambda (u3: T).(\lambda (v3: T).(\lambda (t3: T).(eq T (THead (Bind b)
915 u2 (THead (Flat Appl) (lift (S O) O v2) t2)) (THead (Bind b0) v3 (THead (Flat
916 Appl) (lift (S O) O u3) t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda
917 (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u3)))))))
918 (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
919 (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_: B).(\lambda (_:
920 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1
921 t3)))))))) (ex6_6_intro B T T T T T (\lambda (b0: B).(\lambda (_: T).(\lambda
922 (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b0
923 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
924 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind b) u0 t0) (THead (Bind
925 b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda
926 (u3: T).(\lambda (v3: T).(\lambda (t3: T).(eq T (THead (Bind b) u2 (THead
927 (Flat Appl) (lift (S O) O v2) t2)) (THead (Bind b0) v3 (THead (Flat Appl)
928 (lift (S O) O u3) t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_:
929 T).(\lambda (u3: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u3)))))))
930 (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
931 (v3: T).(\lambda (_: T).(pr0 y1 v3))))))) (\lambda (_: B).(\lambda (_:
932 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1
933 t3))))))) b u0 t0 v2 u2 t2 H1 (refl_equal T (THead (Bind b) u0 t0))
934 (refl_equal T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)))
935 H13 H4 H6)) t1 H10)))))))) H9))))))))))))))))) (\lambda (u0: T).(\lambda (u2:
936 T).(\lambda (_: (pr0 u0 u2)).(\lambda (_: (((eq T u0 (THead (Flat Appl) u1
937 t1)) \to (or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead
938 (Flat Appl) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
939 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (ex4_4 T T T T (\lambda (y1:
940 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
941 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
942 (t2: T).(eq T u2 (THead (Bind Abbr) u3 t2)))))) (\lambda (_: T).(\lambda (_:
943 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
944 (z1: T).(\lambda (_: T).(\lambda (t2: T).(pr0 z1 t2)))))) (ex6_6 B T T T T T
945 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
946 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
947 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
948 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
949 T).(\lambda (u3: T).(\lambda (v2: T).(\lambda (t2: T).(eq T u2 (THead (Bind
950 b) v2 (THead (Flat Appl) (lift (S O) O u3) t2))))))))) (\lambda (_:
951 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
952 (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
953 T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2)))))))
954 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
955 T).(\lambda (t2: T).(pr0 z1 t2)))))))))))).(\lambda (t0: T).(\lambda (t2:
956 T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Flat Appl) u1
957 t1)) \to (or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead
958 (Flat Appl) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
959 (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1:
960 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
961 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
962 (t3: T).(eq T t2 (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_:
963 T).(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda
964 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
965 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
966 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
967 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
968 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
969 T).(\lambda (u3: T).(\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
970 b) v2 (THead (Flat Appl) (lift (S O) O u3) t3))))))))) (\lambda (_:
971 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda (_: T).(\lambda
972 (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
973 T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2)))))))
974 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
975 T).(\lambda (t3: T).(pr0 z1 t3)))))))))))).(\lambda (w: T).(\lambda (_:
976 (subst0 O u2 t2 w)).(\lambda (H6: (eq T (THead (Bind Abbr) u0 t0) (THead
977 (Flat Appl) u1 t1))).(let H7 \def (eq_ind T (THead (Bind Abbr) u0 t0)
978 (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
979 \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _)
980 \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat Appl) u1
981 t1) H6) in (False_ind (or3 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T
982 (THead (Bind Abbr) u2 w) (THead (Flat Appl) u3 t3)))) (\lambda (u3:
983 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
984 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
985 T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
986 T).(\lambda (_: T).(\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind Abbr)
987 u2 w) (THead (Bind Abbr) u3 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda
988 (u3: T).(\lambda (_: T).(pr0 u1 u3))))) (\lambda (_: T).(\lambda (z1:
989 T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
990 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
991 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
992 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
993 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
994 T).(\lambda (u3: T).(\lambda (v2: T).(\lambda (t3: T).(eq T (THead (Bind
995 Abbr) u2 w) (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u3)
996 t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u3:
997 T).(\lambda (_: T).(\lambda (_: T).(pr0 u1 u3))))))) (\lambda (_: B).(\lambda
998 (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0
999 y1 v2))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_:
1000 T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3))))))))) H7)))))))))))))
1001 (\lambda (b: B).(\lambda (_: (not (eq B b Abst))).(\lambda (t0: T).(\lambda
1002 (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Flat Appl)
1003 u1 t1)) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead
1004 (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
1005 (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1:
1006 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
1007 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1008 (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
1009 T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
1010 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
1011 (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1012 T).(\lambda (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1:
1013 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
1014 (THead (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
1015 T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
1016 b0) v2 (THead (Flat Appl) (lift (S O) O u2) t3))))))))) (\lambda (_:
1017 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda
1018 (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1019 T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2)))))))
1020 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
1021 T).(\lambda (t3: T).(pr0 z1 t3)))))))))))).(\lambda (u: T).(\lambda (H4: (eq
1022 T (THead (Bind b) u (lift (S O) O t0)) (THead (Flat Appl) u1 t1))).(let H5
1023 \def (eq_ind T (THead (Bind b) u (lift (S O) O t0)) (\lambda (ee: T).(match
1024 ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k
1025 _ _) \Rightarrow (match k with [(Bind _) \Rightarrow True | (Flat _)
1026 \Rightarrow False])])) I (THead (Flat Appl) u1 t1) H4) in (False_ind (or3
1027 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2
1028 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
1029 T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
1030 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1
1031 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3:
1032 T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
1033 T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda
1034 (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T
1035 (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1036 T).(\lambda (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1:
1037 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1
1038 (THead (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
1039 T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
1040 b0) v2 (THead (Flat Appl) (lift (S O) O u2) t3))))))))) (\lambda (_:
1041 B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda
1042 (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1043 T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2)))))))
1044 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
1045 T).(\lambda (t3: T).(pr0 z1 t3))))))))) H5)))))))))) (\lambda (t0:
1046 T).(\lambda (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead
1047 (Flat Appl) u1 t1)) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq
1048 T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1
1049 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda
1050 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead
1051 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1052 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_:
1053 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))))) (\lambda
1054 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3))))))
1055 (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
1056 (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
1057 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1058 (_: T).(eq T t1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
1059 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t3: T).(eq T
1060 t2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t3)))))))))
1061 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
1062 T).(\lambda (_: T).(pr0 u1 u2))))))) (\lambda (_: B).(\lambda (y1:
1063 T).(\lambda (_: T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1
1064 v2))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_:
1065 T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))))))))).(\lambda (u:
1066 T).(\lambda (H3: (eq T (THead (Flat Cast) u t0) (THead (Flat Appl) u1
1067 t1))).(let H4 \def (eq_ind T (THead (Flat Cast) u t0) (\lambda (ee: T).(match
1068 ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k
1069 _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat f)
1070 \Rightarrow (match f with [Appl \Rightarrow False | Cast \Rightarrow
1071 True])])])) I (THead (Flat Appl) u1 t1) H3) in (False_ind (or3 (ex3_2 T T
1072 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3))))
1073 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
1074 T).(pr0 t1 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
1075 (_: T).(\lambda (_: T).(eq T t1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
1076 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
1077 Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1078 (_: T).(pr0 u1 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
1079 T).(\lambda (t3: T).(pr0 z1 t3)))))) (ex6_6 B T T T T T (\lambda (b:
1080 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1081 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
1082 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t1 (THead (Bind
1083 b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
1084 (u2: T).(\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind b) v2 (THead
1085 (Flat Appl) (lift (S O) O u2) t3))))))))) (\lambda (_: B).(\lambda (_:
1086 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 u1
1087 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
1088 T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_:
1089 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1090 (t3: T).(pr0 z1 t3))))))))) H4)))))))) y x H0))) H)))).
1093 \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Flat Cast) u1
1094 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead
1095 (Flat Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
1096 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 x)))))
1098 \lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (H: (pr0 (THead
1099 (Flat Cast) u1 t1) x)).(insert_eq T (THead (Flat Cast) u1 t1) (\lambda (t:
1100 T).(pr0 t x)) (\lambda (_: T).(or (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
1101 T).(eq T x (THead (Flat Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0
1102 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 x)))
1103 (\lambda (y: T).(\lambda (H0: (pr0 y x)).(pr0_ind (\lambda (t: T).(\lambda
1104 (t0: T).((eq T t (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u2:
1105 T).(\lambda (t2: T).(eq T t0 (THead (Flat Cast) u2 t2)))) (\lambda (u2:
1106 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1
1107 t2)))) (pr0 t1 t0))))) (\lambda (t: T).(\lambda (H1: (eq T t (THead (Flat
1108 Cast) u1 t1))).(let H2 \def (f_equal T T (\lambda (e: T).e) t (THead (Flat
1109 Cast) u1 t1) H1) in (eq_ind_r T (THead (Flat Cast) u1 t1) (\lambda (t0:
1110 T).(or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead (Flat
1111 Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
1112 T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 t0))) (or_introl (ex3_2 T T
1113 (\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Flat Cast) u1 t1) (THead
1114 (Flat Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
1115 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 (THead (Flat Cast) u1 t1))
1116 (ex3_2_intro T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Flat Cast)
1117 u1 t1) (THead (Flat Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1
1118 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2))) u1 t1 (refl_equal T
1119 (THead (Flat Cast) u1 t1)) (pr0_refl u1) (pr0_refl t1))) t H2)))) (\lambda
1120 (u0: T).(\lambda (u2: T).(\lambda (H1: (pr0 u0 u2)).(\lambda (H2: (((eq T u0
1121 (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2:
1122 T).(eq T u2 (THead (Flat Cast) u3 t2)))) (\lambda (u3: T).(\lambda (_:
1123 T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1
1124 u2))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H3: (pr0 t0 t2)).(\lambda
1125 (H4: (((eq T t0 (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u3:
1126 T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u3 t3)))) (\lambda (u3:
1127 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
1128 t3)))) (pr0 t1 t2))))).(\lambda (k: K).(\lambda (H5: (eq T (THead k u0 t0)
1129 (THead (Flat Cast) u1 t1))).(let H6 \def (f_equal T K (\lambda (e: T).(match
1130 e with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _)
1131 \Rightarrow k0])) (THead k u0 t0) (THead (Flat Cast) u1 t1) H5) in ((let H7
1132 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow u0 |
1133 (TLRef _) \Rightarrow u0 | (THead _ t _) \Rightarrow t])) (THead k u0 t0)
1134 (THead (Flat Cast) u1 t1) H5) in ((let H8 \def (f_equal T T (\lambda (e:
1135 T).(match e with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 |
1136 (THead _ _ t) \Rightarrow t])) (THead k u0 t0) (THead (Flat Cast) u1 t1) H5)
1137 in (\lambda (H9: (eq T u0 u1)).(\lambda (H10: (eq K k (Flat Cast))).(eq_ind_r
1138 K (Flat Cast) (\lambda (k0: K).(or (ex3_2 T T (\lambda (u3: T).(\lambda (t3:
1139 T).(eq T (THead k0 u2 t2) (THead (Flat Cast) u3 t3)))) (\lambda (u3:
1140 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
1141 t3)))) (pr0 t1 (THead k0 u2 t2)))) (let H11 \def (eq_ind T t0 (\lambda (t:
1142 T).((eq T t (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u3:
1143 T).(\lambda (t3: T).(eq T t2 (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 t2)))) H4 t1 H8) in (let H12 \def (eq_ind T t0 (\lambda (t:
1146 T).(pr0 t t2)) H3 t1 H8) in (let H13 \def (eq_ind T u0 (\lambda (t: T).((eq T
1147 t (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda
1148 (t3: T).(eq T u2 (THead (Flat Cast) u3 t3)))) (\lambda (u3: T).(\lambda (_:
1149 T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1
1150 u2)))) H2 u1 H9) in (let H14 \def (eq_ind T u0 (\lambda (t: T).(pr0 t u2)) H1
1151 u1 H9) in (or_introl (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T
1152 (THead (Flat Cast) u2 t2) (THead (Flat Cast) u3 t3)))) (\lambda (u3:
1153 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
1154 t3)))) (pr0 t1 (THead (Flat Cast) u2 t2)) (ex3_2_intro T T (\lambda (u3:
1155 T).(\lambda (t3: T).(eq T (THead (Flat Cast) u2 t2) (THead (Flat Cast) u3
1156 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_:
1157 T).(\lambda (t3: T).(pr0 t1 t3))) u2 t2 (refl_equal T (THead (Flat Cast) u2
1158 t2)) H14 H12)))))) k H10)))) H7)) H6)))))))))))) (\lambda (u: T).(\lambda
1159 (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1
1160 (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
1161 T).(eq T v2 (THead (Flat Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_:
1162 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1
1163 v2))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda
1164 (_: (((eq T t0 (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u2:
1165 T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u2 t3)))) (\lambda (u2:
1166 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
1167 t3)))) (pr0 t1 t2))))).(\lambda (H5: (eq T (THead (Flat Appl) v1 (THead (Bind
1168 Abst) u t0)) (THead (Flat Cast) u1 t1))).(let H6 \def (eq_ind T (THead (Flat
1169 Appl) v1 (THead (Bind Abst) u t0)) (\lambda (ee: T).(match ee with [(TSort _)
1170 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
1171 (match k with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow (match f
1172 with [Appl \Rightarrow True | Cast \Rightarrow False])])])) I (THead (Flat
1173 Cast) u1 t1) H5) in (False_ind (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3:
1174 T).(eq T (THead (Bind Abbr) v2 t2) (THead (Flat Cast) u2 t3)))) (\lambda (u2:
1175 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
1176 t3)))) (pr0 t1 (THead (Bind Abbr) v2 t2))) H6)))))))))))) (\lambda (b:
1177 B).(\lambda (_: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2:
1178 T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Flat Cast) u1
1179 t1)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead
1180 (Flat Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
1181 (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 v2))))).(\lambda (u0:
1182 T).(\lambda (u2: T).(\lambda (_: (pr0 u0 u2)).(\lambda (_: (((eq T u0 (THead
1183 (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq
1184 T u2 (THead (Flat Cast) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1
1185 u3))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1
1186 u2))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda
1187 (_: (((eq T t0 (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u3:
1188 T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u3 t3)))) (\lambda (u3:
1189 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
1190 t3)))) (pr0 t1 t2))))).(\lambda (H8: (eq T (THead (Flat Appl) v1 (THead (Bind
1191 b) u0 t0)) (THead (Flat Cast) u1 t1))).(let H9 \def (eq_ind T (THead (Flat
1192 Appl) v1 (THead (Bind b) u0 t0)) (\lambda (ee: T).(match ee with [(TSort _)
1193 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
1194 (match k with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow (match f
1195 with [Appl \Rightarrow True | Cast \Rightarrow False])])])) I (THead (Flat
1196 Cast) u1 t1) H8) in (False_ind (or (ex3_2 T T (\lambda (u3: T).(\lambda (t3:
1197 T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)) (THead
1198 (Flat Cast) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda
1199 (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (THead (Bind b) u2 (THead
1200 (Flat Appl) (lift (S O) O v2) t2)))) H9))))))))))))))))) (\lambda (u0:
1201 T).(\lambda (u2: T).(\lambda (_: (pr0 u0 u2)).(\lambda (_: (((eq T u0 (THead
1202 (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq
1203 T u2 (THead (Flat Cast) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1
1204 u3))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1
1205 u2))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda
1206 (_: (((eq T t0 (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u3:
1207 T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u3 t3)))) (\lambda (u3:
1208 T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
1209 t3)))) (pr0 t1 t2))))).(\lambda (w: T).(\lambda (_: (subst0 O u2 t2
1210 w)).(\lambda (H6: (eq T (THead (Bind Abbr) u0 t0) (THead (Flat Cast) u1
1211 t1))).(let H7 \def (eq_ind T (THead (Bind Abbr) u0 t0) (\lambda (ee:
1212 T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
1213 | (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow True | (Flat
1214 _) \Rightarrow False])])) I (THead (Flat Cast) u1 t1) H6) in (False_ind (or
1215 (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) u2 w)
1216 (THead (Flat Cast) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3)))
1217 (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (THead (Bind Abbr) u2
1218 w))) H7))))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B b
1219 Abst))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda
1220 (_: (((eq T t0 (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u2:
1221 T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u2 t3)))) (\lambda (u2:
1222 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
1223 t3)))) (pr0 t1 t2))))).(\lambda (u: T).(\lambda (H4: (eq T (THead (Bind b) u
1224 (lift (S O) O t0)) (THead (Flat Cast) u1 t1))).(let H5 \def (eq_ind T (THead
1225 (Bind b) u (lift (S O) O t0)) (\lambda (ee: T).(match ee with [(TSort _)
1226 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
1227 (match k with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I
1228 (THead (Flat Cast) u1 t1) H4) in (False_ind (or (ex3_2 T T (\lambda (u2:
1229 T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u2 t3)))) (\lambda (u2:
1230 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
1231 t3)))) (pr0 t1 t2)) H5)))))))))) (\lambda (t0: T).(\lambda (t2: T).(\lambda
1232 (H1: (pr0 t0 t2)).(\lambda (H2: (((eq T t0 (THead (Flat Cast) u1 t1)) \to (or
1233 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u2
1234 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
1235 T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 t2))))).(\lambda (u: T).(\lambda
1236 (H3: (eq T (THead (Flat Cast) u t0) (THead (Flat Cast) u1 t1))).(let H4 \def
1237 (f_equal T T (\lambda (e: T).(match e 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 with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 |
1241 (THead _ _ t) \Rightarrow t])) (THead (Flat Cast) u t0) (THead (Flat Cast) u1
1242 t1) H3) in (\lambda (_: (eq T u u1)).(let H7 \def (eq_ind T t0 (\lambda (t:
1243 T).((eq T t (THead (Flat Cast) u1 t1)) \to (or (ex3_2 T T (\lambda (u2:
1244 T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) u2 t3)))) (\lambda (u2:
1245 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1
1246 t3)))) (pr0 t1 t2)))) H2 t1 H5) in (let H8 \def (eq_ind T t0 (\lambda (t:
1247 T).(pr0 t t2)) H1 t1 H5) in (or_intror (ex3_2 T T (\lambda (u2: T).(\lambda
1248 (t3: T).(eq T t2 (THead (Flat Cast) u2 t3)))) (\lambda (u2: T).(\lambda (_:
1249 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 t2)
1250 H8))))) H4)))))))) y x H0))) H)))).
1253 \forall (t1: T).(\forall (x: T).(\forall (h: nat).(\forall (d: nat).((pr0
1254 (lift h d t1) x) \to (ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda
1255 (t2: T).(pr0 t1 t2)))))))
1257 \lambda (t1: T).(\lambda (x: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda
1258 (H: (pr0 (lift h d t1) x)).(insert_eq T (lift h d t1) (\lambda (t: T).(pr0 t
1259 x)) (\lambda (_: T).(ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda
1260 (t2: T).(pr0 t1 t2)))) (\lambda (y: T).(\lambda (H0: (pr0 y x)).(unintro nat
1261 d (\lambda (n: nat).((eq T y (lift h n t1)) \to (ex2 T (\lambda (t2: T).(eq T
1262 x (lift h n t2))) (\lambda (t2: T).(pr0 t1 t2))))) (unintro T t1 (\lambda (t:
1263 T).(\forall (x0: nat).((eq T y (lift h x0 t)) \to (ex2 T (\lambda (t2: T).(eq
1264 T x (lift h x0 t2))) (\lambda (t2: T).(pr0 t t2)))))) (pr0_ind (\lambda (t:
1265 T).(\lambda (t0: T).(\forall (x0: T).(\forall (x1: nat).((eq T t (lift h x1
1266 x0)) \to (ex2 T (\lambda (t2: T).(eq T t0 (lift h x1 t2))) (\lambda (t2:
1267 T).(pr0 x0 t2)))))))) (\lambda (t: T).(\lambda (x0: T).(\lambda (x1:
1268 nat).(\lambda (H1: (eq T t (lift h x1 x0))).(ex_intro2 T (\lambda (t2: T).(eq
1269 T t (lift h x1 t2))) (\lambda (t2: T).(pr0 x0 t2)) x0 H1 (pr0_refl x0))))))
1270 (\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (H2:
1271 ((\forall (x0: T).(\forall (x1: nat).((eq T u1 (lift h x1 x0)) \to (ex2 T
1272 (\lambda (t2: T).(eq T u2 (lift h x1 t2))) (\lambda (t2: T).(pr0 x0
1273 t2)))))))).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (pr0 t2
1274 t3)).(\lambda (H4: ((\forall (x0: T).(\forall (x1: nat).((eq T t2 (lift h x1
1275 x0)) \to (ex2 T (\lambda (t4: T).(eq T t3 (lift h x1 t4))) (\lambda (t4:
1276 T).(pr0 x0 t4)))))))).(\lambda (k: K).(\lambda (x0: T).(\lambda (x1:
1277 nat).(\lambda (H5: (eq T (THead k u1 t2) (lift h x1 x0))).(K_ind (\lambda
1278 (k0: K).((eq T (THead k0 u1 t2) (lift h x1 x0)) \to (ex2 T (\lambda (t4:
1279 T).(eq T (THead k0 u2 t3) (lift h x1 t4))) (\lambda (t4: T).(pr0 x0 t4)))))
1280 (\lambda (b: B).(\lambda (H6: (eq T (THead (Bind b) u1 t2) (lift h x1
1281 x0))).(ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T x0 (THead (Bind
1282 b) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T u1 (lift h x1 y0))))
1283 (\lambda (_: T).(\lambda (z: T).(eq T t2 (lift h (S x1) z)))) (ex2 T (\lambda
1284 (t4: T).(eq T (THead (Bind b) u2 t3) (lift h x1 t4))) (\lambda (t4: T).(pr0
1285 x0 t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H7: (eq T x0 (THead
1286 (Bind b) x2 x3))).(\lambda (H8: (eq T u1 (lift h x1 x2))).(\lambda (H9: (eq T
1287 t2 (lift h (S x1) x3))).(eq_ind_r T (THead (Bind b) x2 x3) (\lambda (t:
1288 T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind b) u2 t3) (lift h x1 t4)))
1289 (\lambda (t4: T).(pr0 t t4)))) (ex2_ind T (\lambda (t4: T).(eq T t3 (lift h
1290 (S x1) t4))) (\lambda (t4: T).(pr0 x3 t4)) (ex2 T (\lambda (t4: T).(eq T
1291 (THead (Bind b) u2 t3) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind b)
1292 x2 x3) t4))) (\lambda (x4: T).(\lambda (H_x: (eq T t3 (lift h (S x1)
1293 x4))).(\lambda (H10: (pr0 x3 x4)).(eq_ind_r T (lift h (S x1) x4) (\lambda (t:
1294 T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind b) u2 t) (lift h x1 t4)))
1295 (\lambda (t4: T).(pr0 (THead (Bind b) x2 x3) t4)))) (ex2_ind T (\lambda (t4:
1296 T).(eq T u2 (lift h x1 t4))) (\lambda (t4: T).(pr0 x2 t4)) (ex2 T (\lambda
1297 (t4: T).(eq T (THead (Bind b) u2 (lift h (S x1) x4)) (lift h x1 t4)))
1298 (\lambda (t4: T).(pr0 (THead (Bind b) x2 x3) t4))) (\lambda (x5: T).(\lambda
1299 (H_x0: (eq T u2 (lift h x1 x5))).(\lambda (H11: (pr0 x2 x5)).(eq_ind_r T
1300 (lift h x1 x5) (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind b)
1301 t (lift h (S x1) x4)) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind b)
1302 x2 x3) t4)))) (ex_intro2 T (\lambda (t4: T).(eq T (THead (Bind b) (lift h x1
1303 x5) (lift h (S x1) x4)) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind
1304 b) x2 x3) t4)) (THead (Bind b) x5 x4) (sym_eq T (lift h x1 (THead (Bind b) x5
1305 x4)) (THead (Bind b) (lift h x1 x5) (lift h (S x1) x4)) (lift_bind b x5 x4 h
1306 x1)) (pr0_comp x2 x5 H11 x3 x4 H10 (Bind b))) u2 H_x0)))) (H2 x2 x1 H8)) t3
1307 H_x)))) (H4 x3 (S x1) H9)) x0 H7)))))) (lift_gen_bind b u1 t2 x0 h x1 H6))))
1308 (\lambda (f: F).(\lambda (H6: (eq T (THead (Flat f) u1 t2) (lift h x1
1309 x0))).(ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T x0 (THead (Flat
1310 f) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T u1 (lift h x1 y0))))
1311 (\lambda (_: T).(\lambda (z: T).(eq T t2 (lift h x1 z)))) (ex2 T (\lambda
1312 (t4: T).(eq T (THead (Flat f) u2 t3) (lift h x1 t4))) (\lambda (t4: T).(pr0
1313 x0 t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H7: (eq T x0 (THead
1314 (Flat f) x2 x3))).(\lambda (H8: (eq T u1 (lift h x1 x2))).(\lambda (H9: (eq T
1315 t2 (lift h x1 x3))).(eq_ind_r T (THead (Flat f) x2 x3) (\lambda (t: T).(ex2 T
1316 (\lambda (t4: T).(eq T (THead (Flat f) u2 t3) (lift h x1 t4))) (\lambda (t4:
1317 T).(pr0 t t4)))) (ex2_ind T (\lambda (t4: T).(eq T t3 (lift h x1 t4)))
1318 (\lambda (t4: T).(pr0 x3 t4)) (ex2 T (\lambda (t4: T).(eq T (THead (Flat f)
1319 u2 t3) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat f) x2 x3) t4)))
1320 (\lambda (x4: T).(\lambda (H_x: (eq T t3 (lift h x1 x4))).(\lambda (H10: (pr0
1321 x3 x4)).(eq_ind_r T (lift h x1 x4) (\lambda (t: T).(ex2 T (\lambda (t4:
1322 T).(eq T (THead (Flat f) u2 t) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead
1323 (Flat f) x2 x3) t4)))) (ex2_ind T (\lambda (t4: T).(eq T u2 (lift h x1 t4)))
1324 (\lambda (t4: T).(pr0 x2 t4)) (ex2 T (\lambda (t4: T).(eq T (THead (Flat f)
1325 u2 (lift h x1 x4)) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat f) x2
1326 x3) t4))) (\lambda (x5: T).(\lambda (H_x0: (eq T u2 (lift h x1 x5))).(\lambda
1327 (H11: (pr0 x2 x5)).(eq_ind_r T (lift h x1 x5) (\lambda (t: T).(ex2 T (\lambda
1328 (t4: T).(eq T (THead (Flat f) t (lift h x1 x4)) (lift h x1 t4))) (\lambda
1329 (t4: T).(pr0 (THead (Flat f) x2 x3) t4)))) (ex_intro2 T (\lambda (t4: T).(eq
1330 T (THead (Flat f) (lift h x1 x5) (lift h x1 x4)) (lift h x1 t4))) (\lambda
1331 (t4: T).(pr0 (THead (Flat f) x2 x3) t4)) (THead (Flat f) x5 x4) (sym_eq T
1332 (lift h x1 (THead (Flat f) x5 x4)) (THead (Flat f) (lift h x1 x5) (lift h x1
1333 x4)) (lift_flat f x5 x4 h x1)) (pr0_comp x2 x5 H11 x3 x4 H10 (Flat f))) u2
1334 H_x0)))) (H2 x2 x1 H8)) t3 H_x)))) (H4 x3 x1 H9)) x0 H7)))))) (lift_gen_flat
1335 f u1 t2 x0 h x1 H6)))) k H5))))))))))))) (\lambda (u: T).(\lambda (v1:
1336 T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (H2: ((\forall (x0:
1337 T).(\forall (x1: nat).((eq T v1 (lift h x1 x0)) \to (ex2 T (\lambda (t2:
1338 T).(eq T v2 (lift h x1 t2))) (\lambda (t2: T).(pr0 x0 t2)))))))).(\lambda
1339 (t2: T).(\lambda (t3: T).(\lambda (_: (pr0 t2 t3)).(\lambda (H4: ((\forall
1340 (x0: T).(\forall (x1: nat).((eq T t2 (lift h x1 x0)) \to (ex2 T (\lambda (t4:
1341 T).(eq T t3 (lift h x1 t4))) (\lambda (t4: T).(pr0 x0 t4)))))))).(\lambda
1342 (x0: T).(\lambda (x1: nat).(\lambda (H5: (eq T (THead (Flat Appl) v1 (THead
1343 (Bind Abst) u t2)) (lift h x1 x0))).(ex3_2_ind T T (\lambda (y0: T).(\lambda
1344 (z: T).(eq T x0 (THead (Flat Appl) y0 z)))) (\lambda (y0: T).(\lambda (_:
1345 T).(eq T v1 (lift h x1 y0)))) (\lambda (_: T).(\lambda (z: T).(eq T (THead
1346 (Bind Abst) u t2) (lift h x1 z)))) (ex2 T (\lambda (t4: T).(eq T (THead (Bind
1347 Abbr) v2 t3) (lift h x1 t4))) (\lambda (t4: T).(pr0 x0 t4))) (\lambda (x2:
1348 T).(\lambda (x3: T).(\lambda (H6: (eq T x0 (THead (Flat Appl) x2
1349 x3))).(\lambda (H7: (eq T v1 (lift h x1 x2))).(\lambda (H8: (eq T (THead
1350 (Bind Abst) u t2) (lift h x1 x3))).(eq_ind_r T (THead (Flat Appl) x2 x3)
1351 (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind Abbr) v2 t3) (lift
1352 h x1 t4))) (\lambda (t4: T).(pr0 t t4)))) (ex3_2_ind T T (\lambda (y0:
1353 T).(\lambda (z: T).(eq T x3 (THead (Bind Abst) y0 z)))) (\lambda (y0:
1354 T).(\lambda (_: T).(eq T u (lift h x1 y0)))) (\lambda (_: T).(\lambda (z:
1355 T).(eq T t2 (lift h (S x1) z)))) (ex2 T (\lambda (t4: T).(eq T (THead (Bind
1356 Abbr) v2 t3) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat Appl) x2 x3)
1357 t4))) (\lambda (x4: T).(\lambda (x5: T).(\lambda (H9: (eq T x3 (THead (Bind
1358 Abst) x4 x5))).(\lambda (_: (eq T u (lift h x1 x4))).(\lambda (H11: (eq T t2
1359 (lift h (S x1) x5))).(eq_ind_r T (THead (Bind Abst) x4 x5) (\lambda (t:
1360 T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4)))
1361 (\lambda (t4: T).(pr0 (THead (Flat Appl) x2 t) t4)))) (ex2_ind T (\lambda
1362 (t4: T).(eq T t3 (lift h (S x1) t4))) (\lambda (t4: T).(pr0 x5 t4)) (ex2 T
1363 (\lambda (t4: T).(eq T (THead (Bind Abbr) v2 t3) (lift h x1 t4))) (\lambda
1364 (t4: T).(pr0 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5)) t4))) (\lambda
1365 (x6: T).(\lambda (H_x: (eq T t3 (lift h (S x1) x6))).(\lambda (H12: (pr0 x5
1366 x6)).(eq_ind_r T (lift h (S x1) x6) (\lambda (t: T).(ex2 T (\lambda (t4:
1367 T).(eq T (THead (Bind Abbr) v2 t) (lift h x1 t4))) (\lambda (t4: T).(pr0
1368 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5)) t4)))) (ex2_ind T (\lambda
1369 (t4: T).(eq T v2 (lift h x1 t4))) (\lambda (t4: T).(pr0 x2 t4)) (ex2 T
1370 (\lambda (t4: T).(eq T (THead (Bind Abbr) v2 (lift h (S x1) x6)) (lift h x1
1371 t4))) (\lambda (t4: T).(pr0 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5))
1372 t4))) (\lambda (x7: T).(\lambda (H_x0: (eq T v2 (lift h x1 x7))).(\lambda
1373 (H13: (pr0 x2 x7)).(eq_ind_r T (lift h x1 x7) (\lambda (t: T).(ex2 T (\lambda
1374 (t4: T).(eq T (THead (Bind Abbr) t (lift h (S x1) x6)) (lift h x1 t4)))
1375 (\lambda (t4: T).(pr0 (THead (Flat Appl) x2 (THead (Bind Abst) x4 x5)) t4))))
1376 (ex_intro2 T (\lambda (t4: T).(eq T (THead (Bind Abbr) (lift h x1 x7) (lift h
1377 (S x1) x6)) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat Appl) x2
1378 (THead (Bind Abst) x4 x5)) t4)) (THead (Bind Abbr) x7 x6) (sym_eq T (lift h
1379 x1 (THead (Bind Abbr) x7 x6)) (THead (Bind Abbr) (lift h x1 x7) (lift h (S
1380 x1) x6)) (lift_bind Abbr x7 x6 h x1)) (pr0_beta x4 x2 x7 H13 x5 x6 H12)) v2
1381 H_x0)))) (H2 x2 x1 H7)) t3 H_x)))) (H4 x5 (S x1) H11)) x3 H9))))))
1382 (lift_gen_bind Abst u t2 x3 h x1 H8)) x0 H6)))))) (lift_gen_flat Appl v1
1383 (THead (Bind Abst) u t2) x0 h x1 H5)))))))))))))) (\lambda (b: B).(\lambda
1384 (H1: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0
1385 v1 v2)).(\lambda (H3: ((\forall (x0: T).(\forall (x1: nat).((eq T v1 (lift h
1386 x1 x0)) \to (ex2 T (\lambda (t2: T).(eq T v2 (lift h x1 t2))) (\lambda (t2:
1387 T).(pr0 x0 t2)))))))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1
1388 u2)).(\lambda (H5: ((\forall (x0: T).(\forall (x1: nat).((eq T u1 (lift h x1
1389 x0)) \to (ex2 T (\lambda (t2: T).(eq T u2 (lift h x1 t2))) (\lambda (t2:
1390 T).(pr0 x0 t2)))))))).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (pr0 t2
1391 t3)).(\lambda (H7: ((\forall (x0: T).(\forall (x1: nat).((eq T t2 (lift h x1
1392 x0)) \to (ex2 T (\lambda (t4: T).(eq T t3 (lift h x1 t4))) (\lambda (t4:
1393 T).(pr0 x0 t4)))))))).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H8: (eq T
1394 (THead (Flat Appl) v1 (THead (Bind b) u1 t2)) (lift h x1 x0))).(ex3_2_ind T T
1395 (\lambda (y0: T).(\lambda (z: T).(eq T x0 (THead (Flat Appl) y0 z))))
1396 (\lambda (y0: T).(\lambda (_: T).(eq T v1 (lift h x1 y0)))) (\lambda (_:
1397 T).(\lambda (z: T).(eq T (THead (Bind b) u1 t2) (lift h x1 z)))) (ex2 T
1398 (\lambda (t4: T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O
1399 v2) t3)) (lift h x1 t4))) (\lambda (t4: T).(pr0 x0 t4))) (\lambda (x2:
1400 T).(\lambda (x3: T).(\lambda (H9: (eq T x0 (THead (Flat Appl) x2
1401 x3))).(\lambda (H10: (eq T v1 (lift h x1 x2))).(\lambda (H11: (eq T (THead
1402 (Bind b) u1 t2) (lift h x1 x3))).(eq_ind_r T (THead (Flat Appl) x2 x3)
1403 (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind b) u2 (THead (Flat
1404 Appl) (lift (S O) O v2) t3)) (lift h x1 t4))) (\lambda (t4: T).(pr0 t t4))))
1405 (ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T x3 (THead (Bind b) y0
1406 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T u1 (lift h x1 y0)))) (\lambda
1407 (_: T).(\lambda (z: T).(eq T t2 (lift h (S x1) z)))) (ex2 T (\lambda (t4:
1408 T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)) (lift h
1409 x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat Appl) x2 x3) t4))) (\lambda (x4:
1410 T).(\lambda (x5: T).(\lambda (H12: (eq T x3 (THead (Bind b) x4 x5))).(\lambda
1411 (H13: (eq T u1 (lift h x1 x4))).(\lambda (H14: (eq T t2 (lift h (S x1)
1412 x5))).(eq_ind_r T (THead (Bind b) x4 x5) (\lambda (t: T).(ex2 T (\lambda (t4:
1413 T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3)) (lift h
1414 x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat Appl) x2 t) t4)))) (ex2_ind T
1415 (\lambda (t4: T).(eq T t3 (lift h (S x1) t4))) (\lambda (t4: T).(pr0 x5 t4))
1416 (ex2 T (\lambda (t4: T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S
1417 O) O v2) t3)) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat Appl) x2
1418 (THead (Bind b) x4 x5)) t4))) (\lambda (x6: T).(\lambda (H_x: (eq T t3 (lift
1419 h (S x1) x6))).(\lambda (H15: (pr0 x5 x6)).(eq_ind_r T (lift h (S x1) x6)
1420 (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind b) u2 (THead (Flat
1421 Appl) (lift (S O) O v2) t)) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead
1422 (Flat Appl) x2 (THead (Bind b) x4 x5)) t4)))) (ex2_ind T (\lambda (t4: T).(eq
1423 T u2 (lift h x1 t4))) (\lambda (t4: T).(pr0 x4 t4)) (ex2 T (\lambda (t4:
1424 T).(eq T (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) (lift h (S
1425 x1) x6))) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat Appl) x2 (THead
1426 (Bind b) x4 x5)) t4))) (\lambda (x7: T).(\lambda (H_x0: (eq T u2 (lift h x1
1427 x7))).(\lambda (H16: (pr0 x4 x7)).(eq_ind_r T (lift h x1 x7) (\lambda (t:
1428 T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind b) t (THead (Flat Appl) (lift
1429 (S O) O v2) (lift h (S x1) x6))) (lift h x1 t4))) (\lambda (t4: T).(pr0
1430 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4)))) (ex2_ind T (\lambda (t4:
1431 T).(eq T v2 (lift h x1 t4))) (\lambda (t4: T).(pr0 x2 t4)) (ex2 T (\lambda
1432 (t4: T).(eq T (THead (Bind b) (lift h x1 x7) (THead (Flat Appl) (lift (S O) O
1433 v2) (lift h (S x1) x6))) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat
1434 Appl) x2 (THead (Bind b) x4 x5)) t4))) (\lambda (x8: T).(\lambda (H_x1: (eq T
1435 v2 (lift h x1 x8))).(\lambda (H17: (pr0 x2 x8)).(eq_ind_r T (lift h x1 x8)
1436 (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind b) (lift h x1 x7)
1437 (THead (Flat Appl) (lift (S O) O t) (lift h (S x1) x6))) (lift h x1 t4)))
1438 (\lambda (t4: T).(pr0 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4))))
1439 (eq_ind T (lift h (plus (S O) x1) (lift (S O) O x8)) (\lambda (t: T).(ex2 T
1440 (\lambda (t4: T).(eq T (THead (Bind b) (lift h x1 x7) (THead (Flat Appl) t
1441 (lift h (S x1) x6))) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat
1442 Appl) x2 (THead (Bind b) x4 x5)) t4)))) (eq_ind T (lift h (S x1) (THead (Flat
1443 Appl) (lift (S O) O x8) x6)) (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T
1444 (THead (Bind b) (lift h x1 x7) t) (lift h x1 t4))) (\lambda (t4: T).(pr0
1445 (THead (Flat Appl) x2 (THead (Bind b) x4 x5)) t4)))) (ex_intro2 T (\lambda
1446 (t4: T).(eq T (THead (Bind b) (lift h x1 x7) (lift h (S x1) (THead (Flat
1447 Appl) (lift (S O) O x8) x6))) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead
1448 (Flat Appl) x2 (THead (Bind b) x4 x5)) t4)) (THead (Bind b) x7 (THead (Flat
1449 Appl) (lift (S O) O x8) x6)) (sym_eq T (lift h x1 (THead (Bind b) x7 (THead
1450 (Flat Appl) (lift (S O) O x8) x6))) (THead (Bind b) (lift h x1 x7) (lift h (S
1451 x1) (THead (Flat Appl) (lift (S O) O x8) x6))) (lift_bind b x7 (THead (Flat
1452 Appl) (lift (S O) O x8) x6) h x1)) (pr0_upsilon b H1 x2 x8 H17 x4 x7 H16 x5
1453 x6 H15)) (THead (Flat Appl) (lift h (S x1) (lift (S O) O x8)) (lift h (S x1)
1454 x6)) (lift_flat Appl (lift (S O) O x8) x6 h (S x1))) (lift (S O) O (lift h x1
1455 x8)) (lift_d x8 h (S O) x1 O (le_O_n x1))) v2 H_x1)))) (H3 x2 x1 H10)) u2
1456 H_x0)))) (H5 x4 x1 H13)) t3 H_x)))) (H7 x5 (S x1) H14)) x3 H12))))))
1457 (lift_gen_bind b u1 t2 x3 h x1 H11)) x0 H9)))))) (lift_gen_flat Appl v1
1458 (THead (Bind b) u1 t2) x0 h x1 H8))))))))))))))))))) (\lambda (u1:
1459 T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda (H2: ((\forall (x0:
1460 T).(\forall (x1: nat).((eq T u1 (lift h x1 x0)) \to (ex2 T (\lambda (t2:
1461 T).(eq T u2 (lift h x1 t2))) (\lambda (t2: T).(pr0 x0 t2)))))))).(\lambda
1462 (t2: T).(\lambda (t3: T).(\lambda (_: (pr0 t2 t3)).(\lambda (H4: ((\forall
1463 (x0: T).(\forall (x1: nat).((eq T t2 (lift h x1 x0)) \to (ex2 T (\lambda (t4:
1464 T).(eq T t3 (lift h x1 t4))) (\lambda (t4: T).(pr0 x0 t4)))))))).(\lambda (w:
1465 T).(\lambda (H5: (subst0 O u2 t3 w)).(\lambda (x0: T).(\lambda (x1:
1466 nat).(\lambda (H6: (eq T (THead (Bind Abbr) u1 t2) (lift h x1
1467 x0))).(ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T x0 (THead (Bind
1468 Abbr) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T u1 (lift h x1 y0))))
1469 (\lambda (_: T).(\lambda (z: T).(eq T t2 (lift h (S x1) z)))) (ex2 T (\lambda
1470 (t4: T).(eq T (THead (Bind Abbr) u2 w) (lift h x1 t4))) (\lambda (t4: T).(pr0
1471 x0 t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H7: (eq T x0 (THead
1472 (Bind Abbr) x2 x3))).(\lambda (H8: (eq T u1 (lift h x1 x2))).(\lambda (H9:
1473 (eq T t2 (lift h (S x1) x3))).(eq_ind_r T (THead (Bind Abbr) x2 x3) (\lambda
1474 (t: T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind Abbr) u2 w) (lift h x1
1475 t4))) (\lambda (t4: T).(pr0 t t4)))) (ex2_ind T (\lambda (t4: T).(eq T t3
1476 (lift h (S x1) t4))) (\lambda (t4: T).(pr0 x3 t4)) (ex2 T (\lambda (t4:
1477 T).(eq T (THead (Bind Abbr) u2 w) (lift h x1 t4))) (\lambda (t4: T).(pr0
1478 (THead (Bind Abbr) x2 x3) t4))) (\lambda (x4: T).(\lambda (H_x: (eq T t3
1479 (lift h (S x1) x4))).(\lambda (H10: (pr0 x3 x4)).(let H11 \def (eq_ind T t3
1480 (\lambda (t: T).(subst0 O u2 t w)) H5 (lift h (S x1) x4) H_x) in (ex2_ind T
1481 (\lambda (t4: T).(eq T u2 (lift h x1 t4))) (\lambda (t4: T).(pr0 x2 t4)) (ex2
1482 T (\lambda (t4: T).(eq T (THead (Bind Abbr) u2 w) (lift h x1 t4))) (\lambda
1483 (t4: T).(pr0 (THead (Bind Abbr) x2 x3) t4))) (\lambda (x5: T).(\lambda (H_x0:
1484 (eq T u2 (lift h x1 x5))).(\lambda (H12: (pr0 x2 x5)).(eq_ind_r T (lift h x1
1485 x5) (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind Abbr) t w)
1486 (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind Abbr) x2 x3) t4)))) (let
1487 H13 \def (eq_ind T u2 (\lambda (t: T).(subst0 O t (lift h (S x1) x4) w)) H11
1488 (lift h x1 x5) H_x0) in (let H14 \def (refl_equal nat (S (plus O x1))) in
1489 (let H15 \def (eq_ind nat (S x1) (\lambda (n: nat).(subst0 O (lift h x1 x5)
1490 (lift h n x4) w)) H13 (S (plus O x1)) H14) in (ex2_ind T (\lambda (t4: T).(eq
1491 T w (lift h (S (plus O x1)) t4))) (\lambda (t4: T).(subst0 O x5 x4 t4)) (ex2
1492 T (\lambda (t4: T).(eq T (THead (Bind Abbr) (lift h x1 x5) w) (lift h x1
1493 t4))) (\lambda (t4: T).(pr0 (THead (Bind Abbr) x2 x3) t4))) (\lambda (x6:
1494 T).(\lambda (H16: (eq T w (lift h (S (plus O x1)) x6))).(\lambda (H17:
1495 (subst0 O x5 x4 x6)).(eq_ind_r T (lift h (S (plus O x1)) x6) (\lambda (t:
1496 T).(ex2 T (\lambda (t4: T).(eq T (THead (Bind Abbr) (lift h x1 x5) t) (lift h
1497 x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind Abbr) x2 x3) t4)))) (ex_intro2 T
1498 (\lambda (t4: T).(eq T (THead (Bind Abbr) (lift h x1 x5) (lift h (S (plus O
1499 x1)) x6)) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind Abbr) x2 x3)
1500 t4)) (THead (Bind Abbr) x5 x6) (sym_eq T (lift h x1 (THead (Bind Abbr) x5
1501 x6)) (THead (Bind Abbr) (lift h x1 x5) (lift h (S (plus O x1)) x6))
1502 (lift_bind Abbr x5 x6 h (plus O x1))) (pr0_delta x2 x5 H12 x3 x4 H10 x6 H17))
1503 w H16)))) (subst0_gen_lift_lt x5 x4 w O h x1 H15))))) u2 H_x0)))) (H2 x2 x1
1504 H8)))))) (H4 x3 (S x1) H9)) x0 H7)))))) (lift_gen_bind Abbr u1 t2 x0 h x1
1505 H6))))))))))))))) (\lambda (b: B).(\lambda (H1: (not (eq B b Abst))).(\lambda
1506 (t2: T).(\lambda (t3: T).(\lambda (_: (pr0 t2 t3)).(\lambda (H3: ((\forall
1507 (x0: T).(\forall (x1: nat).((eq T t2 (lift h x1 x0)) \to (ex2 T (\lambda (t4:
1508 T).(eq T t3 (lift h x1 t4))) (\lambda (t4: T).(pr0 x0 t4)))))))).(\lambda (u:
1509 T).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H4: (eq T (THead (Bind b) u
1510 (lift (S O) O t2)) (lift h x1 x0))).(ex3_2_ind T T (\lambda (y0: T).(\lambda
1511 (z: T).(eq T x0 (THead (Bind b) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq
1512 T u (lift h x1 y0)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift (S O) O t2)
1513 (lift h (S x1) z)))) (ex2 T (\lambda (t4: T).(eq T t3 (lift h x1 t4)))
1514 (\lambda (t4: T).(pr0 x0 t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda
1515 (H5: (eq T x0 (THead (Bind b) x2 x3))).(\lambda (_: (eq T u (lift h x1
1516 x2))).(\lambda (H7: (eq T (lift (S O) O t2) (lift h (S x1) x3))).(eq_ind_r T
1517 (THead (Bind b) x2 x3) (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T t3 (lift
1518 h x1 t4))) (\lambda (t4: T).(pr0 t t4)))) (let H8 \def (eq_ind_r nat (plus (S
1519 O) x1) (\lambda (n: nat).(eq nat (S x1) n)) (le_antisym (S x1) (plus (S O)
1520 x1) (le_n (plus (S O) x1)) (le_n (S x1))) (plus x1 (S O)) (plus_sym x1 (S
1521 O))) in (let H9 \def (eq_ind nat (S x1) (\lambda (n: nat).(eq T (lift (S O) O
1522 t2) (lift h n x3))) H7 (plus x1 (S O)) H8) in (ex2_ind T (\lambda (t4: T).(eq
1523 T x3 (lift (S O) O t4))) (\lambda (t4: T).(eq T t2 (lift h x1 t4))) (ex2 T
1524 (\lambda (t4: T).(eq T t3 (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind
1525 b) x2 x3) t4))) (\lambda (x4: T).(\lambda (H10: (eq T x3 (lift (S O) O
1526 x4))).(\lambda (H11: (eq T t2 (lift h x1 x4))).(eq_ind_r T (lift (S O) O x4)
1527 (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T t3 (lift h x1 t4))) (\lambda
1528 (t4: T).(pr0 (THead (Bind b) x2 t) t4)))) (ex2_ind T (\lambda (t4: T).(eq T
1529 t3 (lift h x1 t4))) (\lambda (t4: T).(pr0 x4 t4)) (ex2 T (\lambda (t4: T).(eq
1530 T t3 (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind b) x2 (lift (S O) O
1531 x4)) t4))) (\lambda (x5: T).(\lambda (H_x: (eq T t3 (lift h x1 x5))).(\lambda
1532 (H12: (pr0 x4 x5)).(eq_ind_r T (lift h x1 x5) (\lambda (t: T).(ex2 T (\lambda
1533 (t4: T).(eq T t (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind b) x2
1534 (lift (S O) O x4)) t4)))) (ex_intro2 T (\lambda (t4: T).(eq T (lift h x1 x5)
1535 (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Bind b) x2 (lift (S O) O x4))
1536 t4)) x5 (refl_equal T (lift h x1 x5)) (pr0_zeta b H1 x4 x5 H12 x2)) t3
1537 H_x)))) (H3 x4 x1 H11)) x3 H10)))) (lift_gen_lift t2 x3 (S O) h O x1 (le_O_n
1538 x1) H9)))) x0 H5)))))) (lift_gen_bind b u (lift (S O) O t2) x0 h x1
1539 H4)))))))))))) (\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (pr0 t2
1540 t3)).(\lambda (H2: ((\forall (x0: T).(\forall (x1: nat).((eq T t2 (lift h x1
1541 x0)) \to (ex2 T (\lambda (t4: T).(eq T t3 (lift h x1 t4))) (\lambda (t4:
1542 T).(pr0 x0 t4)))))))).(\lambda (u: T).(\lambda (x0: T).(\lambda (x1:
1543 nat).(\lambda (H3: (eq T (THead (Flat Cast) u t2) (lift h x1 x0))).(ex3_2_ind
1544 T T (\lambda (y0: T).(\lambda (z: T).(eq T x0 (THead (Flat Cast) y0 z))))
1545 (\lambda (y0: T).(\lambda (_: T).(eq T u (lift h x1 y0)))) (\lambda (_:
1546 T).(\lambda (z: T).(eq T t2 (lift h x1 z)))) (ex2 T (\lambda (t4: T).(eq T t3
1547 (lift h x1 t4))) (\lambda (t4: T).(pr0 x0 t4))) (\lambda (x2: T).(\lambda
1548 (x3: T).(\lambda (H4: (eq T x0 (THead (Flat Cast) x2 x3))).(\lambda (_: (eq T
1549 u (lift h x1 x2))).(\lambda (H6: (eq T t2 (lift h x1 x3))).(eq_ind_r T (THead
1550 (Flat Cast) x2 x3) (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T t3 (lift h
1551 x1 t4))) (\lambda (t4: T).(pr0 t t4)))) (ex2_ind T (\lambda (t4: T).(eq T t3
1552 (lift h x1 t4))) (\lambda (t4: T).(pr0 x3 t4)) (ex2 T (\lambda (t4: T).(eq T
1553 t3 (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat Cast) x2 x3) t4)))
1554 (\lambda (x4: T).(\lambda (H_x: (eq T t3 (lift h x1 x4))).(\lambda (H7: (pr0
1555 x3 x4)).(eq_ind_r T (lift h x1 x4) (\lambda (t: T).(ex2 T (\lambda (t4:
1556 T).(eq T t (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat Cast) x2 x3)
1557 t4)))) (ex_intro2 T (\lambda (t4: T).(eq T (lift h x1 x4) (lift h x1 t4)))
1558 (\lambda (t4: T).(pr0 (THead (Flat Cast) x2 x3) t4)) x4 (refl_equal T (lift h
1559 x1 x4)) (pr0_tau x3 x4 H7 x2)) t3 H_x)))) (H2 x3 x1 H6)) x0 H4))))))
1560 (lift_gen_flat Cast u t2 x0 h x1 H3)))))))))) y x H0))))) H))))).
projects / helm.git / blob