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