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