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/dec".
21 include "subst0/dec.ma".
28 \forall (t1: T).(or (\forall (t2: T).((pr0 t1 t2) \to (eq T t1 t2))) (ex2 T
29 (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2:
32 \lambda (t1: T).(T_ind (\lambda (t: T).(or (\forall (t2: T).((pr0 t t2) \to
33 (eq T t t2))) (ex2 T (\lambda (t2: T).((eq T t t2) \to (\forall (P:
34 Prop).P))) (\lambda (t2: T).(pr0 t t2))))) (\lambda (n: nat).(or_introl
35 (\forall (t2: T).((pr0 (TSort n) t2) \to (eq T (TSort n) t2))) (ex2 T
36 (\lambda (t2: T).((eq T (TSort n) t2) \to (\forall (P: Prop).P))) (\lambda
37 (t2: T).(pr0 (TSort n) t2))) (\lambda (t2: T).(\lambda (H: (pr0 (TSort n)
38 t2)).(eq_ind_r T (TSort n) (\lambda (t: T).(eq T (TSort n) t)) (refl_equal T
39 (TSort n)) t2 (pr0_gen_sort t2 n H)))))) (\lambda (n: nat).(or_introl
40 (\forall (t2: T).((pr0 (TLRef n) t2) \to (eq T (TLRef n) t2))) (ex2 T
41 (\lambda (t2: T).((eq T (TLRef n) t2) \to (\forall (P: Prop).P))) (\lambda
42 (t2: T).(pr0 (TLRef n) t2))) (\lambda (t2: T).(\lambda (H: (pr0 (TLRef n)
43 t2)).(eq_ind_r T (TLRef n) (\lambda (t: T).(eq T (TLRef n) t)) (refl_equal T
44 (TLRef n)) t2 (pr0_gen_lref t2 n H)))))) (\lambda (k: K).(\lambda (t:
45 T).(\lambda (H: (or (\forall (t2: T).((pr0 t t2) \to (eq T t t2))) (ex2 T
46 (\lambda (t2: T).((eq T t t2) \to (\forall (P: Prop).P))) (\lambda (t2:
47 T).(pr0 t t2))))).(\lambda (t0: T).(\lambda (H0: (or (\forall (t2: T).((pr0
48 t0 t2) \to (eq T t0 t2))) (ex2 T (\lambda (t2: T).((eq T t0 t2) \to (\forall
49 (P: Prop).P))) (\lambda (t2: T).(pr0 t0 t2))))).(match k in K return (\lambda
50 (k0: K).(or (\forall (t2: T).((pr0 (THead k0 t t0) t2) \to (eq T (THead k0 t
51 t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead k0 t t0) t2) \to (\forall (P:
52 Prop).P))) (\lambda (t2: T).(pr0 (THead k0 t t0) t2))))) with [(Bind b)
53 \Rightarrow (match b in B return (\lambda (b0: B).(or (\forall (t2: T).((pr0
54 (THead (Bind b0) t t0) t2) \to (eq T (THead (Bind b0) t t0) t2))) (ex2 T
55 (\lambda (t2: T).((eq T (THead (Bind b0) t t0) t2) \to (\forall (P:
56 Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind b0) t t0) t2))))) with [Abbr
57 \Rightarrow (or_intror (\forall (t2: T).((pr0 (THead (Bind Abbr) t t0) t2)
58 \to (eq T (THead (Bind Abbr) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T
59 (THead (Bind Abbr) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2:
60 T).(pr0 (THead (Bind Abbr) t t0) t2))) (let H_x \def (dnf_dec t t0 O) in (let
61 H1 \def H_x in (ex_ind T (\lambda (v: T).(or (subst0 O t t0 (lift (S O) O v))
62 (eq T t0 (lift (S O) O v)))) (ex2 T (\lambda (t2: T).((eq T (THead (Bind
63 Abbr) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead
64 (Bind Abbr) t t0) t2))) (\lambda (x: T).(\lambda (H2: (or (subst0 O t t0
65 (lift (S O) O x)) (eq T t0 (lift (S O) O x)))).(or_ind (subst0 O t t0 (lift
66 (S O) O x)) (eq T t0 (lift (S O) O x)) (ex2 T (\lambda (t2: T).((eq T (THead
67 (Bind Abbr) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0
68 (THead (Bind Abbr) t t0) t2))) (\lambda (H3: (subst0 O t t0 (lift (S O) O
69 x))).(ex_intro2 T (\lambda (t2: T).((eq T (THead (Bind Abbr) t t0) t2) \to
70 (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Abbr) t t0) t2))
71 (THead (Bind Abbr) t (lift (S O) O x)) (\lambda (H4: (eq T (THead (Bind Abbr)
72 t t0) (THead (Bind Abbr) t (lift (S O) O x)))).(\lambda (P: Prop).(let H5
73 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
74 with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t2)
75 \Rightarrow t2])) (THead (Bind Abbr) t t0) (THead (Bind Abbr) t (lift (S O) O
76 x)) H4) in (let H6 \def (eq_ind T t0 (\lambda (t2: T).(subst0 O t t2 (lift (S
77 O) O x))) H3 (lift (S O) O x) H5) in (subst0_refl t (lift (S O) O x) O H6
78 P))))) (pr0_delta t t (pr0_refl t) t0 t0 (pr0_refl t0) (lift (S O) O x) H3)))
79 (\lambda (H3: (eq T t0 (lift (S O) O x))).(eq_ind_r T (lift (S O) O x)
80 (\lambda (t2: T).(ex2 T (\lambda (t3: T).((eq T (THead (Bind Abbr) t t2) t3)
81 \to (\forall (P: Prop).P))) (\lambda (t3: T).(pr0 (THead (Bind Abbr) t t2)
82 t3)))) (ex_intro2 T (\lambda (t2: T).((eq T (THead (Bind Abbr) t (lift (S O)
83 O x)) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind
84 Abbr) t (lift (S O) O x)) t2)) x (\lambda (H4: (eq T (THead (Bind Abbr) t
85 (lift (S O) O x)) x)).(\lambda (P: Prop).(thead_x_lift_y_y (Bind Abbr) x t (S
86 O) O H4 P))) (pr0_zeta Abbr not_abbr_abst x x (pr0_refl x) t)) t0 H3)) H2)))
87 H1)))) | Abst \Rightarrow (let H1 \def H in (or_ind (\forall (t2: T).((pr0 t
88 t2) \to (eq T t t2))) (ex2 T (\lambda (t2: T).((eq T t t2) \to (\forall (P:
89 Prop).P))) (\lambda (t2: T).(pr0 t t2))) (or (\forall (t2: T).((pr0 (THead
90 (Bind Abst) t t0) t2) \to (eq T (THead (Bind Abst) t t0) t2))) (ex2 T
91 (\lambda (t2: T).((eq T (THead (Bind Abst) t t0) t2) \to (\forall (P:
92 Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Abst) t t0) t2)))) (\lambda
93 (H2: ((\forall (t2: T).((pr0 t t2) \to (eq T t t2))))).(let H3 \def H0 in
94 (or_ind (\forall (t2: T).((pr0 t0 t2) \to (eq T t0 t2))) (ex2 T (\lambda (t2:
95 T).((eq T t0 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t0 t2)))
96 (or (\forall (t2: T).((pr0 (THead (Bind Abst) t t0) t2) \to (eq T (THead
97 (Bind Abst) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Bind Abst) t
98 t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Abst)
99 t t0) t2)))) (\lambda (H4: ((\forall (t2: T).((pr0 t0 t2) \to (eq T t0
100 t2))))).(or_introl (\forall (t2: T).((pr0 (THead (Bind Abst) t t0) t2) \to
101 (eq T (THead (Bind Abst) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead
102 (Bind Abst) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0
103 (THead (Bind Abst) t t0) t2))) (\lambda (t2: T).(\lambda (H5: (pr0 (THead
104 (Bind Abst) t t0) t2)).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t3: T).(eq T
105 t2 (THead (Bind Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 t u2)))
106 (\lambda (_: T).(\lambda (t3: T).(pr0 t0 t3))) (eq T (THead (Bind Abst) t t0)
107 t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H6: (eq T t2 (THead (Bind
108 Abst) x0 x1))).(\lambda (H7: (pr0 t x0)).(\lambda (H8: (pr0 t0 x1)).(let H_y
109 \def (H4 x1 H8) in (let H_y0 \def (H2 x0 H7) in (let H9 \def (eq_ind_r T x1
110 (\lambda (t3: T).(pr0 t0 t3)) H8 t0 H_y) in (let H10 \def (eq_ind_r T x1
111 (\lambda (t3: T).(eq T t2 (THead (Bind Abst) x0 t3))) H6 t0 H_y) in (let H11
112 \def (eq_ind_r T x0 (\lambda (t3: T).(pr0 t t3)) H7 t H_y0) in (let H12 \def
113 (eq_ind_r T x0 (\lambda (t3: T).(eq T t2 (THead (Bind Abst) t3 t0))) H10 t
114 H_y0) in (eq_ind_r T (THead (Bind Abst) t t0) (\lambda (t3: T).(eq T (THead
115 (Bind Abst) t t0) t3)) (refl_equal T (THead (Bind Abst) t t0)) t2
116 H12)))))))))))) (pr0_gen_abst t t0 t2 H5)))))) (\lambda (H4: (ex2 T (\lambda
117 (t2: T).((eq T t0 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t0
118 t2)))).(ex2_ind T (\lambda (t2: T).((eq T t0 t2) \to (\forall (P: Prop).P)))
119 (\lambda (t2: T).(pr0 t0 t2)) (or (\forall (t2: T).((pr0 (THead (Bind Abst) t
120 t0) t2) \to (eq T (THead (Bind Abst) t t0) t2))) (ex2 T (\lambda (t2: T).((eq
121 T (THead (Bind Abst) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2:
122 T).(pr0 (THead (Bind Abst) t t0) t2)))) (\lambda (x: T).(\lambda (H5: (((eq T
123 t0 x) \to (\forall (P: Prop).P)))).(\lambda (H6: (pr0 t0 x)).(or_intror
124 (\forall (t2: T).((pr0 (THead (Bind Abst) t t0) t2) \to (eq T (THead (Bind
125 Abst) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Bind Abst) t t0) t2)
126 \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Abst) t t0)
127 t2))) (ex_intro2 T (\lambda (t2: T).((eq T (THead (Bind Abst) t t0) t2) \to
128 (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Abst) t t0) t2))
129 (THead (Bind Abst) t x) (\lambda (H7: (eq T (THead (Bind Abst) t t0) (THead
130 (Bind Abst) t x))).(\lambda (P: Prop).(let H8 \def (f_equal T T (\lambda (e:
131 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 |
132 (TLRef _) \Rightarrow t0 | (THead _ _ t2) \Rightarrow t2])) (THead (Bind
133 Abst) t t0) (THead (Bind Abst) t x) H7) in (let H9 \def (eq_ind_r T x
134 (\lambda (t2: T).(pr0 t0 t2)) H6 t0 H8) in (let H10 \def (eq_ind_r T x
135 (\lambda (t2: T).((eq T t0 t2) \to (\forall (P0: Prop).P0))) H5 t0 H8) in
136 (H10 (refl_equal T t0) P)))))) (pr0_comp t t (pr0_refl t) t0 x H6 (Bind
137 Abst))))))) H4)) H3))) (\lambda (H2: (ex2 T (\lambda (t2: T).((eq T t t2) \to
138 (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t t2)))).(ex2_ind T (\lambda
139 (t2: T).((eq T t t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t t2))
140 (or (\forall (t2: T).((pr0 (THead (Bind Abst) t t0) t2) \to (eq T (THead
141 (Bind Abst) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Bind Abst) t
142 t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Abst)
143 t t0) t2)))) (\lambda (x: T).(\lambda (H3: (((eq T t x) \to (\forall (P:
144 Prop).P)))).(\lambda (H4: (pr0 t x)).(or_intror (\forall (t2: T).((pr0 (THead
145 (Bind Abst) t t0) t2) \to (eq T (THead (Bind Abst) t t0) t2))) (ex2 T
146 (\lambda (t2: T).((eq T (THead (Bind Abst) t t0) t2) \to (\forall (P:
147 Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Abst) t t0) t2))) (ex_intro2 T
148 (\lambda (t2: T).((eq T (THead (Bind Abst) t t0) t2) \to (\forall (P:
149 Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Abst) t t0) t2)) (THead (Bind
150 Abst) x t0) (\lambda (H5: (eq T (THead (Bind Abst) t t0) (THead (Bind Abst) x
151 t0))).(\lambda (P: Prop).(let H6 \def (f_equal T T (\lambda (e: T).(match e
152 in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t | (TLRef _)
153 \Rightarrow t | (THead _ t2 _) \Rightarrow t2])) (THead (Bind Abst) t t0)
154 (THead (Bind Abst) x t0) H5) in (let H7 \def (eq_ind_r T x (\lambda (t2:
155 T).(pr0 t t2)) H4 t H6) in (let H8 \def (eq_ind_r T x (\lambda (t2: T).((eq T
156 t t2) \to (\forall (P0: Prop).P0))) H3 t H6) in (H8 (refl_equal T t) P))))))
157 (pr0_comp t x H4 t0 t0 (pr0_refl t0) (Bind Abst))))))) H2)) H1)) | Void
158 \Rightarrow (let H_x \def (dnf_dec t t0 O) in (let H1 \def H_x in (ex_ind T
159 (\lambda (v: T).(or (subst0 O t t0 (lift (S O) O v)) (eq T t0 (lift (S O) O
160 v)))) (or (\forall (t2: T).((pr0 (THead (Bind Void) t t0) t2) \to (eq T
161 (THead (Bind Void) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Bind
162 Void) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead
163 (Bind Void) t t0) t2)))) (\lambda (x: T).(\lambda (H2: (or (subst0 O t t0
164 (lift (S O) O x)) (eq T t0 (lift (S O) O x)))).(or_ind (subst0 O t t0 (lift
165 (S O) O x)) (eq T t0 (lift (S O) O x)) (or (\forall (t2: T).((pr0 (THead
166 (Bind Void) t t0) t2) \to (eq T (THead (Bind Void) t t0) t2))) (ex2 T
167 (\lambda (t2: T).((eq T (THead (Bind Void) t t0) t2) \to (\forall (P:
168 Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Void) t t0) t2)))) (\lambda
169 (H3: (subst0 O t t0 (lift (S O) O x))).(let H4 \def H in (or_ind (\forall
170 (t2: T).((pr0 t t2) \to (eq T t t2))) (ex2 T (\lambda (t2: T).((eq T t t2)
171 \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t t2))) (or (\forall (t2:
172 T).((pr0 (THead (Bind Void) t t0) t2) \to (eq T (THead (Bind Void) t t0)
173 t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Bind Void) t t0) t2) \to
174 (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Void) t t0) t2))))
175 (\lambda (H5: ((\forall (t2: T).((pr0 t t2) \to (eq T t t2))))).(let H6 \def
176 H0 in (or_ind (\forall (t2: T).((pr0 t0 t2) \to (eq T t0 t2))) (ex2 T
177 (\lambda (t2: T).((eq T t0 t2) \to (\forall (P: Prop).P))) (\lambda (t2:
178 T).(pr0 t0 t2))) (or (\forall (t2: T).((pr0 (THead (Bind Void) t t0) t2) \to
179 (eq T (THead (Bind Void) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead
180 (Bind Void) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0
181 (THead (Bind Void) t t0) t2)))) (\lambda (H7: ((\forall (t2: T).((pr0 t0 t2)
182 \to (eq T t0 t2))))).(or_introl (\forall (t2: T).((pr0 (THead (Bind Void) t
183 t0) t2) \to (eq T (THead (Bind Void) t t0) t2))) (ex2 T (\lambda (t2: T).((eq
184 T (THead (Bind Void) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2:
185 T).(pr0 (THead (Bind Void) t t0) t2))) (\lambda (t2: T).(\lambda (H8: (pr0
186 (THead (Bind Void) t t0) t2)).(or_ind (ex3_2 T T (\lambda (u2: T).(\lambda
187 (t3: T).(eq T t2 (THead (Bind Void) u2 t3)))) (\lambda (u2: T).(\lambda (_:
188 T).(pr0 t u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t0 t3)))) (pr0 t0 (lift
189 (S O) O t2)) (eq T (THead (Bind Void) t t0) t2) (\lambda (H9: (ex3_2 T T
190 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u2 t3))))
191 (\lambda (u2: T).(\lambda (_: T).(pr0 t u2))) (\lambda (_: T).(\lambda (t3:
192 T).(pr0 t0 t3))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2
193 (THead (Bind Void) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 t u2)))
194 (\lambda (_: T).(\lambda (t3: T).(pr0 t0 t3))) (eq T (THead (Bind Void) t t0)
195 t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H10: (eq T t2 (THead (Bind
196 Void) x0 x1))).(\lambda (H11: (pr0 t x0)).(\lambda (H12: (pr0 t0 x1)).(let
197 H_y \def (H7 x1 H12) in (let H_y0 \def (H5 x0 H11) in (let H13 \def (eq_ind_r
198 T x1 (\lambda (t3: T).(pr0 t0 t3)) H12 t0 H_y) in (let H14 \def (eq_ind_r T
199 x1 (\lambda (t3: T).(eq T t2 (THead (Bind Void) x0 t3))) H10 t0 H_y) in (let
200 H15 \def (eq_ind_r T x0 (\lambda (t3: T).(pr0 t t3)) H11 t H_y0) in (let H16
201 \def (eq_ind_r T x0 (\lambda (t3: T).(eq T t2 (THead (Bind Void) t3 t0))) H14
202 t H_y0) in (eq_ind_r T (THead (Bind Void) t t0) (\lambda (t3: T).(eq T (THead
203 (Bind Void) t t0) t3)) (refl_equal T (THead (Bind Void) t t0)) t2
204 H16)))))))))))) H9)) (\lambda (H9: (pr0 t0 (lift (S O) O t2))).(let H_y \def
205 (H7 (lift (S O) O t2) H9) in (let H10 \def (eq_ind T t0 (\lambda (t3:
206 T).(subst0 O t t3 (lift (S O) O x))) H3 (lift (S O) O t2) H_y) in (eq_ind_r T
207 (lift (S O) O t2) (\lambda (t3: T).(eq T (THead (Bind Void) t t3) t2))
208 (subst0_gen_lift_false t2 t (lift (S O) O x) (S O) O O (le_n O) (eq_ind_r nat
209 (plus (S O) O) (\lambda (n: nat).(lt O n)) (le_n (plus (S O) O)) (plus O (S
210 O)) (plus_comm O (S O))) H10 (eq T (THead (Bind Void) t (lift (S O) O t2))
211 t2)) t0 H_y)))) (pr0_gen_void t t0 t2 H8)))))) (\lambda (H7: (ex2 T (\lambda
212 (t2: T).((eq T t0 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t0
213 t2)))).(ex2_ind T (\lambda (t2: T).((eq T t0 t2) \to (\forall (P: Prop).P)))
214 (\lambda (t2: T).(pr0 t0 t2)) (or (\forall (t2: T).((pr0 (THead (Bind Void) t
215 t0) t2) \to (eq T (THead (Bind Void) t t0) t2))) (ex2 T (\lambda (t2: T).((eq
216 T (THead (Bind Void) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2:
217 T).(pr0 (THead (Bind Void) t t0) t2)))) (\lambda (x0: T).(\lambda (H8: (((eq
218 T t0 x0) \to (\forall (P: Prop).P)))).(\lambda (H9: (pr0 t0 x0)).(or_intror
219 (\forall (t2: T).((pr0 (THead (Bind Void) t t0) t2) \to (eq T (THead (Bind
220 Void) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Bind Void) t t0) t2)
221 \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Void) t t0)
222 t2))) (ex_intro2 T (\lambda (t2: T).((eq T (THead (Bind Void) t t0) t2) \to
223 (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Void) t t0) t2))
224 (THead (Bind Void) t x0) (\lambda (H10: (eq T (THead (Bind Void) t t0) (THead
225 (Bind Void) t x0))).(\lambda (P: Prop).(let H11 \def (f_equal T T (\lambda
226 (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0
227 | (TLRef _) \Rightarrow t0 | (THead _ _ t2) \Rightarrow t2])) (THead (Bind
228 Void) t t0) (THead (Bind Void) t x0) H10) in (let H12 \def (eq_ind_r T x0
229 (\lambda (t2: T).(pr0 t0 t2)) H9 t0 H11) in (let H13 \def (eq_ind_r T x0
230 (\lambda (t2: T).((eq T t0 t2) \to (\forall (P0: Prop).P0))) H8 t0 H11) in
231 (H13 (refl_equal T t0) P)))))) (pr0_comp t t (pr0_refl t) t0 x0 H9 (Bind
232 Void))))))) H7)) H6))) (\lambda (H5: (ex2 T (\lambda (t2: T).((eq T t t2) \to
233 (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t t2)))).(ex2_ind T (\lambda
234 (t2: T).((eq T t t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t t2))
235 (or (\forall (t2: T).((pr0 (THead (Bind Void) t t0) t2) \to (eq T (THead
236 (Bind Void) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Bind Void) t
237 t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Void)
238 t t0) t2)))) (\lambda (x0: T).(\lambda (H6: (((eq T t x0) \to (\forall (P:
239 Prop).P)))).(\lambda (H7: (pr0 t x0)).(or_intror (\forall (t2: T).((pr0
240 (THead (Bind Void) t t0) t2) \to (eq T (THead (Bind Void) t t0) t2))) (ex2 T
241 (\lambda (t2: T).((eq T (THead (Bind Void) t t0) t2) \to (\forall (P:
242 Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Void) t t0) t2))) (ex_intro2 T
243 (\lambda (t2: T).((eq T (THead (Bind Void) t t0) t2) \to (\forall (P:
244 Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Void) t t0) t2)) (THead (Bind
245 Void) x0 t0) (\lambda (H8: (eq T (THead (Bind Void) t t0) (THead (Bind Void)
246 x0 t0))).(\lambda (P: Prop).(let H9 \def (f_equal T T (\lambda (e: T).(match
247 e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t | (TLRef _)
248 \Rightarrow t | (THead _ t2 _) \Rightarrow t2])) (THead (Bind Void) t t0)
249 (THead (Bind Void) x0 t0) H8) in (let H10 \def (eq_ind_r T x0 (\lambda (t2:
250 T).(pr0 t t2)) H7 t H9) in (let H11 \def (eq_ind_r T x0 (\lambda (t2: T).((eq
251 T t t2) \to (\forall (P0: Prop).P0))) H6 t H9) in (H11 (refl_equal T t)
252 P)))))) (pr0_comp t x0 H7 t0 t0 (pr0_refl t0) (Bind Void))))))) H5)) H4)))
253 (\lambda (H3: (eq T t0 (lift (S O) O x))).(let H4 \def (eq_ind T t0 (\lambda
254 (t2: T).(or (\forall (t3: T).((pr0 t2 t3) \to (eq T t2 t3))) (ex2 T (\lambda
255 (t3: T).((eq T t2 t3) \to (\forall (P: Prop).P))) (\lambda (t3: T).(pr0 t2
256 t3))))) H0 (lift (S O) O x) H3) in (eq_ind_r T (lift (S O) O x) (\lambda (t2:
257 T).(or (\forall (t3: T).((pr0 (THead (Bind Void) t t2) t3) \to (eq T (THead
258 (Bind Void) t t2) t3))) (ex2 T (\lambda (t3: T).((eq T (THead (Bind Void) t
259 t2) t3) \to (\forall (P: Prop).P))) (\lambda (t3: T).(pr0 (THead (Bind Void)
260 t t2) t3))))) (or_intror (\forall (t2: T).((pr0 (THead (Bind Void) t (lift (S
261 O) O x)) t2) \to (eq T (THead (Bind Void) t (lift (S O) O x)) t2))) (ex2 T
262 (\lambda (t2: T).((eq T (THead (Bind Void) t (lift (S O) O x)) t2) \to
263 (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Void) t (lift (S
264 O) O x)) t2))) (ex_intro2 T (\lambda (t2: T).((eq T (THead (Bind Void) t
265 (lift (S O) O x)) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0
266 (THead (Bind Void) t (lift (S O) O x)) t2)) x (\lambda (H5: (eq T (THead
267 (Bind Void) t (lift (S O) O x)) x)).(\lambda (P: Prop).(thead_x_lift_y_y
268 (Bind Void) x t (S O) O H5 P))) (pr0_zeta Void not_void_abst x x (pr0_refl x)
269 t))) t0 H3))) H2))) H1)))]) | (Flat f) \Rightarrow (match f in F return
270 (\lambda (f0: F).(or (\forall (t2: T).((pr0 (THead (Flat f0) t t0) t2) \to
271 (eq T (THead (Flat f0) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead
272 (Flat f0) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead
273 (Flat f0) t t0) t2))))) with [Appl \Rightarrow (let H_x \def (binder_dec t0)
274 in (let H1 \def H_x in (or_ind (ex_3 B T T (\lambda (b: B).(\lambda (w:
275 T).(\lambda (u: T).(eq T t0 (THead (Bind b) w u)))))) (\forall (b:
276 B).(\forall (w: T).(\forall (u: T).((eq T t0 (THead (Bind b) w u)) \to
277 (\forall (P: Prop).P))))) (or (\forall (t2: T).((pr0 (THead (Flat Appl) t t0)
278 t2) \to (eq T (THead (Flat Appl) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T
279 (THead (Flat Appl) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2:
280 T).(pr0 (THead (Flat Appl) t t0) t2)))) (\lambda (H2: (ex_3 B T T (\lambda
281 (b: B).(\lambda (w: T).(\lambda (u: T).(eq T t0 (THead (Bind b) w
282 u))))))).(ex_3_ind B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(eq
283 T t0 (THead (Bind b) w u))))) (or (\forall (t2: T).((pr0 (THead (Flat Appl) t
284 t0) t2) \to (eq T (THead (Flat Appl) t t0) t2))) (ex2 T (\lambda (t2: T).((eq
285 T (THead (Flat Appl) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2:
286 T).(pr0 (THead (Flat Appl) t t0) t2)))) (\lambda (x0: B).(\lambda (x1:
287 T).(\lambda (x2: T).(\lambda (H3: (eq T t0 (THead (Bind x0) x1 x2))).(let H4
288 \def (eq_ind T t0 (\lambda (t2: T).(or (\forall (t3: T).((pr0 t2 t3) \to (eq
289 T t2 t3))) (ex2 T (\lambda (t3: T).((eq T t2 t3) \to (\forall (P: Prop).P)))
290 (\lambda (t3: T).(pr0 t2 t3))))) H0 (THead (Bind x0) x1 x2) H3) in (eq_ind_r
291 T (THead (Bind x0) x1 x2) (\lambda (t2: T).(or (\forall (t3: T).((pr0 (THead
292 (Flat Appl) t t2) t3) \to (eq T (THead (Flat Appl) t t2) t3))) (ex2 T
293 (\lambda (t3: T).((eq T (THead (Flat Appl) t t2) t3) \to (\forall (P:
294 Prop).P))) (\lambda (t3: T).(pr0 (THead (Flat Appl) t t2) t3))))) ((match x0
295 in B return (\lambda (b: B).((or (\forall (t2: T).((pr0 (THead (Bind b) x1
296 x2) t2) \to (eq T (THead (Bind b) x1 x2) t2))) (ex2 T (\lambda (t2: T).((eq T
297 (THead (Bind b) x1 x2) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0
298 (THead (Bind b) x1 x2) t2)))) \to (or (\forall (t2: T).((pr0 (THead (Flat
299 Appl) t (THead (Bind b) x1 x2)) t2) \to (eq T (THead (Flat Appl) t (THead
300 (Bind b) x1 x2)) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t
301 (THead (Bind b) x1 x2)) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0
302 (THead (Flat Appl) t (THead (Bind b) x1 x2)) t2)))))) with [Abbr \Rightarrow
303 (\lambda (_: (or (\forall (t2: T).((pr0 (THead (Bind Abbr) x1 x2) t2) \to (eq
304 T (THead (Bind Abbr) x1 x2) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Bind
305 Abbr) x1 x2) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead
306 (Bind Abbr) x1 x2) t2))))).(or_intror (\forall (t2: T).((pr0 (THead (Flat
307 Appl) t (THead (Bind Abbr) x1 x2)) t2) \to (eq T (THead (Flat Appl) t (THead
308 (Bind Abbr) x1 x2)) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t
309 (THead (Bind Abbr) x1 x2)) t2) \to (\forall (P: Prop).P))) (\lambda (t2:
310 T).(pr0 (THead (Flat Appl) t (THead (Bind Abbr) x1 x2)) t2))) (ex_intro2 T
311 (\lambda (t2: T).((eq T (THead (Flat Appl) t (THead (Bind Abbr) x1 x2)) t2)
312 \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t (THead
313 (Bind Abbr) x1 x2)) t2)) (THead (Bind Abbr) x1 (THead (Flat Appl) (lift (S O)
314 O t) x2)) (\lambda (H6: (eq T (THead (Flat Appl) t (THead (Bind Abbr) x1 x2))
315 (THead (Bind Abbr) x1 (THead (Flat Appl) (lift (S O) O t) x2)))).(\lambda (P:
316 Prop).(let H7 \def (eq_ind T (THead (Flat Appl) t (THead (Bind Abbr) x1 x2))
317 (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
318 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ t2) \Rightarrow
319 (match t2 in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False
320 | (TLRef _) \Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in K
321 return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _)
322 \Rightarrow False])])])) I (THead (Bind Abbr) x1 (THead (Flat Appl) (lift (S
323 O) O t) x2)) H6) in (False_ind P H7)))) (pr0_upsilon Abbr not_abbr_abst t t
324 (pr0_refl t) x1 x1 (pr0_refl x1) x2 x2 (pr0_refl x2))))) | Abst \Rightarrow
325 (\lambda (_: (or (\forall (t2: T).((pr0 (THead (Bind Abst) x1 x2) t2) \to (eq
326 T (THead (Bind Abst) x1 x2) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Bind
327 Abst) x1 x2) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead
328 (Bind Abst) x1 x2) t2))))).(or_intror (\forall (t2: T).((pr0 (THead (Flat
329 Appl) t (THead (Bind Abst) x1 x2)) t2) \to (eq T (THead (Flat Appl) t (THead
330 (Bind Abst) x1 x2)) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t
331 (THead (Bind Abst) x1 x2)) t2) \to (\forall (P: Prop).P))) (\lambda (t2:
332 T).(pr0 (THead (Flat Appl) t (THead (Bind Abst) x1 x2)) t2))) (ex_intro2 T
333 (\lambda (t2: T).((eq T (THead (Flat Appl) t (THead (Bind Abst) x1 x2)) t2)
334 \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t (THead
335 (Bind Abst) x1 x2)) t2)) (THead (Bind Abbr) t x2) (\lambda (H6: (eq T (THead
336 (Flat Appl) t (THead (Bind Abst) x1 x2)) (THead (Bind Abbr) t x2))).(\lambda
337 (P: Prop).(let H7 \def (eq_ind T (THead (Flat Appl) t (THead (Bind Abst) x1
338 x2)) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with
339 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k0 _ _)
340 \Rightarrow (match k0 in K return (\lambda (_: K).Prop) with [(Bind _)
341 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind Abbr) t x2)
342 H6) in (False_ind P H7)))) (pr0_beta x1 t t (pr0_refl t) x2 x2 (pr0_refl
343 x2))))) | Void \Rightarrow (\lambda (_: (or (\forall (t2: T).((pr0 (THead
344 (Bind Void) x1 x2) t2) \to (eq T (THead (Bind Void) x1 x2) t2))) (ex2 T
345 (\lambda (t2: T).((eq T (THead (Bind Void) x1 x2) t2) \to (\forall (P:
346 Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind Void) x1 x2) t2))))).(or_intror
347 (\forall (t2: T).((pr0 (THead (Flat Appl) t (THead (Bind Void) x1 x2)) t2)
348 \to (eq T (THead (Flat Appl) t (THead (Bind Void) x1 x2)) t2))) (ex2 T
349 (\lambda (t2: T).((eq T (THead (Flat Appl) t (THead (Bind Void) x1 x2)) t2)
350 \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t (THead
351 (Bind Void) x1 x2)) t2))) (ex_intro2 T (\lambda (t2: T).((eq T (THead (Flat
352 Appl) t (THead (Bind Void) x1 x2)) t2) \to (\forall (P: Prop).P))) (\lambda
353 (t2: T).(pr0 (THead (Flat Appl) t (THead (Bind Void) x1 x2)) t2)) (THead
354 (Bind Void) x1 (THead (Flat Appl) (lift (S O) O t) x2)) (\lambda (H6: (eq T
355 (THead (Flat Appl) t (THead (Bind Void) x1 x2)) (THead (Bind Void) x1 (THead
356 (Flat Appl) (lift (S O) O t) x2)))).(\lambda (P: Prop).(let H7 \def (eq_ind T
357 (THead (Flat Appl) t (THead (Bind Void) x1 x2)) (\lambda (ee: T).(match ee in
358 T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
359 \Rightarrow False | (THead _ _ t2) \Rightarrow (match t2 in T return (\lambda
360 (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
361 | (THead k0 _ _) \Rightarrow (match k0 in K return (\lambda (_: K).Prop) with
362 [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])])) I (THead (Bind
363 Void) x1 (THead (Flat Appl) (lift (S O) O t) x2)) H6) in (False_ind P H7))))
364 (pr0_upsilon Void not_void_abst t t (pr0_refl t) x1 x1 (pr0_refl x1) x2 x2
365 (pr0_refl x2)))))]) H4) t0 H3)))))) H2)) (\lambda (H2: ((\forall (b:
366 B).(\forall (w: T).(\forall (u: T).((eq T t0 (THead (Bind b) w u)) \to
367 (\forall (P: Prop).P))))))).(let H3 \def H in (or_ind (\forall (t2: T).((pr0
368 t t2) \to (eq T t t2))) (ex2 T (\lambda (t2: T).((eq T t t2) \to (\forall (P:
369 Prop).P))) (\lambda (t2: T).(pr0 t t2))) (or (\forall (t2: T).((pr0 (THead
370 (Flat Appl) t t0) t2) \to (eq T (THead (Flat Appl) t t0) t2))) (ex2 T
371 (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to (\forall (P:
372 Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2)))) (\lambda
373 (H4: ((\forall (t2: T).((pr0 t t2) \to (eq T t t2))))).(let H5 \def H0 in
374 (or_ind (\forall (t2: T).((pr0 t0 t2) \to (eq T t0 t2))) (ex2 T (\lambda (t2:
375 T).((eq T t0 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t0 t2)))
376 (or (\forall (t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to (eq T (THead
377 (Flat Appl) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t
378 t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl)
379 t t0) t2)))) (\lambda (H6: ((\forall (t2: T).((pr0 t0 t2) \to (eq T t0
380 t2))))).(or_introl (\forall (t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to
381 (eq T (THead (Flat Appl) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead
382 (Flat Appl) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0
383 (THead (Flat Appl) t t0) t2))) (\lambda (t2: T).(\lambda (H7: (pr0 (THead
384 (Flat Appl) t t0) t2)).(or3_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t3:
385 T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_:
386 T).(pr0 t u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t0 t3)))) (ex4_4 T T T
387 T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t0
388 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
389 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_:
390 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 t u2))))) (\lambda
391 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3))))))
392 (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
393 (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
394 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
395 (_: T).(eq T t0 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
396 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t3: T).(eq T
397 t2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t3)))))))))
398 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
399 T).(\lambda (_: T).(pr0 t u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda
400 (_: T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2)))))))
401 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
402 T).(\lambda (t3: T).(pr0 z1 t3)))))))) (eq T (THead (Flat Appl) t t0) t2)
403 (\lambda (H8: (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead
404 (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 t u2))) (\lambda
405 (_: T).(\lambda (t3: T).(pr0 t0 t3))))).(ex3_2_ind T T (\lambda (u2:
406 T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2:
407 T).(\lambda (_: T).(pr0 t u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t0
408 t3))) (eq T (THead (Flat Appl) t t0) t2) (\lambda (x0: T).(\lambda (x1:
409 T).(\lambda (H9: (eq T t2 (THead (Flat Appl) x0 x1))).(\lambda (H10: (pr0 t
410 x0)).(\lambda (H11: (pr0 t0 x1)).(let H_y \def (H6 x1 H11) in (let H_y0 \def
411 (H4 x0 H10) in (let H12 \def (eq_ind_r T x1 (\lambda (t3: T).(pr0 t0 t3)) H11
412 t0 H_y) in (let H13 \def (eq_ind_r T x1 (\lambda (t3: T).(eq T t2 (THead
413 (Flat Appl) x0 t3))) H9 t0 H_y) in (let H14 \def (eq_ind_r T x0 (\lambda (t3:
414 T).(pr0 t t3)) H10 t H_y0) in (let H15 \def (eq_ind_r T x0 (\lambda (t3:
415 T).(eq T t2 (THead (Flat Appl) t3 t0))) H13 t H_y0) in (eq_ind_r T (THead
416 (Flat Appl) t t0) (\lambda (t3: T).(eq T (THead (Flat Appl) t t0) t3))
417 (refl_equal T (THead (Flat Appl) t t0)) t2 H15)))))))))))) H8)) (\lambda (H8:
418 (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
419 T).(eq T t0 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_:
420 T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3))))))
421 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 t
422 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3:
423 T).(pr0 z1 t3))))))).(ex4_4_ind T T T T (\lambda (y1: T).(\lambda (z1:
424 T).(\lambda (_: T).(\lambda (_: T).(eq T t0 (THead (Bind Abst) y1 z1))))))
425 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2
426 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
427 T).(\lambda (_: T).(pr0 t u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda
428 (_: T).(\lambda (t3: T).(pr0 z1 t3))))) (eq T (THead (Flat Appl) t t0) t2)
429 (\lambda (x0: T).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda
430 (H9: (eq T t0 (THead (Bind Abst) x0 x1))).(\lambda (H10: (eq T t2 (THead
431 (Bind Abbr) x2 x3))).(\lambda (_: (pr0 t x2)).(\lambda (_: (pr0 x1
432 x3)).(eq_ind_r T (THead (Bind Abbr) x2 x3) (\lambda (t3: T).(eq T (THead
433 (Flat Appl) t t0) t3)) (let H13 \def (eq_ind T t0 (\lambda (t3: T).(\forall
434 (t4: T).((pr0 t3 t4) \to (eq T t3 t4)))) H6 (THead (Bind Abst) x0 x1) H9) in
435 (let H14 \def (eq_ind T t0 (\lambda (t3: T).(\forall (b: B).(\forall (w:
436 T).(\forall (u: T).((eq T t3 (THead (Bind b) w u)) \to (\forall (P:
437 Prop).P)))))) H2 (THead (Bind Abst) x0 x1) H9) in (eq_ind_r T (THead (Bind
438 Abst) x0 x1) (\lambda (t3: T).(eq T (THead (Flat Appl) t t3) (THead (Bind
439 Abbr) x2 x3))) (H14 Abst x0 x1 (H13 (THead (Bind Abst) x0 x1) (pr0_refl
440 (THead (Bind Abst) x0 x1))) (eq T (THead (Flat Appl) t (THead (Bind Abst) x0
441 x1)) (THead (Bind Abbr) x2 x3))) t0 H9))) t2 H10))))))))) H8)) (\lambda (H8:
442 (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
443 (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
444 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
445 (_: T).(eq T t0 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
446 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t3: T).(eq T
447 t2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t3)))))))))
448 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
449 T).(\lambda (_: T).(pr0 t u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda
450 (_: T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2)))))))
451 (\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
452 T).(\lambda (t3: T).(pr0 z1 t3))))))))).(ex6_6_ind B T T T T T (\lambda (b:
453 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
454 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
455 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T t0 (THead (Bind
456 b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
457 (u2: T).(\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind b) v2 (THead
458 (Flat Appl) (lift (S O) O u2) t3))))))))) (\lambda (_: B).(\lambda (_:
459 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 t
460 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
461 T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_:
462 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
463 (t3: T).(pr0 z1 t3))))))) (eq T (THead (Flat Appl) t t0) t2) (\lambda (x0:
464 B).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4:
465 T).(\lambda (x5: T).(\lambda (_: (not (eq B x0 Abst))).(\lambda (H10: (eq T
466 t0 (THead (Bind x0) x1 x2))).(\lambda (H11: (eq T t2 (THead (Bind x0) x4
467 (THead (Flat Appl) (lift (S O) O x3) x5)))).(\lambda (_: (pr0 t x3)).(\lambda
468 (_: (pr0 x1 x4)).(\lambda (_: (pr0 x2 x5)).(eq_ind_r T (THead (Bind x0) x4
469 (THead (Flat Appl) (lift (S O) O x3) x5)) (\lambda (t3: T).(eq T (THead (Flat
470 Appl) t t0) t3)) (let H15 \def (eq_ind T t0 (\lambda (t3: T).(\forall (t4:
471 T).((pr0 t3 t4) \to (eq T t3 t4)))) H6 (THead (Bind x0) x1 x2) H10) in (let
472 H16 \def (eq_ind T t0 (\lambda (t3: T).(\forall (b: B).(\forall (w:
473 T).(\forall (u: T).((eq T t3 (THead (Bind b) w u)) \to (\forall (P:
474 Prop).P)))))) H2 (THead (Bind x0) x1 x2) H10) in (eq_ind_r T (THead (Bind x0)
475 x1 x2) (\lambda (t3: T).(eq T (THead (Flat Appl) t t3) (THead (Bind x0) x4
476 (THead (Flat Appl) (lift (S O) O x3) x5)))) (H16 x0 x1 x2 (H15 (THead (Bind
477 x0) x1 x2) (pr0_refl (THead (Bind x0) x1 x2))) (eq T (THead (Flat Appl) t
478 (THead (Bind x0) x1 x2)) (THead (Bind x0) x4 (THead (Flat Appl) (lift (S O) O
479 x3) x5)))) t0 H10))) t2 H11))))))))))))) H8)) (pr0_gen_appl t t0 t2 H7))))))
480 (\lambda (H6: (ex2 T (\lambda (t2: T).((eq T t0 t2) \to (\forall (P:
481 Prop).P))) (\lambda (t2: T).(pr0 t0 t2)))).(ex2_ind T (\lambda (t2: T).((eq T
482 t0 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t0 t2)) (or (\forall
483 (t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to (eq T (THead (Flat Appl) t t0)
484 t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to
485 (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2))))
486 (\lambda (x: T).(\lambda (H7: (((eq T t0 x) \to (\forall (P:
487 Prop).P)))).(\lambda (H8: (pr0 t0 x)).(or_intror (\forall (t2: T).((pr0
488 (THead (Flat Appl) t t0) t2) \to (eq T (THead (Flat Appl) t t0) t2))) (ex2 T
489 (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to (\forall (P:
490 Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2))) (ex_intro2 T
491 (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to (\forall (P:
492 Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2)) (THead (Flat
493 Appl) t x) (\lambda (H9: (eq T (THead (Flat Appl) t t0) (THead (Flat Appl) t
494 x))).(\lambda (P: Prop).(let H10 \def (f_equal T T (\lambda (e: T).(match e
495 in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _)
496 \Rightarrow t0 | (THead _ _ t2) \Rightarrow t2])) (THead (Flat Appl) t t0)
497 (THead (Flat Appl) t x) H9) in (let H11 \def (eq_ind_r T x (\lambda (t2:
498 T).(pr0 t0 t2)) H8 t0 H10) in (let H12 \def (eq_ind_r T x (\lambda (t2:
499 T).((eq T t0 t2) \to (\forall (P0: Prop).P0))) H7 t0 H10) in (H12 (refl_equal
500 T t0) P)))))) (pr0_comp t t (pr0_refl t) t0 x H8 (Flat Appl))))))) H6)) H5)))
501 (\lambda (H4: (ex2 T (\lambda (t2: T).((eq T t t2) \to (\forall (P:
502 Prop).P))) (\lambda (t2: T).(pr0 t t2)))).(ex2_ind T (\lambda (t2: T).((eq T
503 t t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t t2)) (or (\forall
504 (t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to (eq T (THead (Flat Appl) t t0)
505 t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to
506 (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2))))
507 (\lambda (x: T).(\lambda (H5: (((eq T t x) \to (\forall (P:
508 Prop).P)))).(\lambda (H6: (pr0 t x)).(or_intror (\forall (t2: T).((pr0 (THead
509 (Flat Appl) t t0) t2) \to (eq T (THead (Flat Appl) t t0) t2))) (ex2 T
510 (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to (\forall (P:
511 Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2))) (ex_intro2 T
512 (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to (\forall (P:
513 Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2)) (THead (Flat
514 Appl) x t0) (\lambda (H7: (eq T (THead (Flat Appl) t t0) (THead (Flat Appl) x
515 t0))).(\lambda (P: Prop).(let H8 \def (f_equal T T (\lambda (e: T).(match e
516 in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t | (TLRef _)
517 \Rightarrow t | (THead _ t2 _) \Rightarrow t2])) (THead (Flat Appl) t t0)
518 (THead (Flat Appl) x t0) H7) in (let H9 \def (eq_ind_r T x (\lambda (t2:
519 T).(pr0 t t2)) H6 t H8) in (let H10 \def (eq_ind_r T x (\lambda (t2: T).((eq
520 T t t2) \to (\forall (P0: Prop).P0))) H5 t H8) in (H10 (refl_equal T t)
521 P)))))) (pr0_comp t x H6 t0 t0 (pr0_refl t0) (Flat Appl))))))) H4)) H3)))
522 H1))) | Cast \Rightarrow (or_intror (\forall (t2: T).((pr0 (THead (Flat Cast)
523 t t0) t2) \to (eq T (THead (Flat Cast) t t0) t2))) (ex2 T (\lambda (t2:
524 T).((eq T (THead (Flat Cast) t t0) t2) \to (\forall (P: Prop).P))) (\lambda
525 (t2: T).(pr0 (THead (Flat Cast) t t0) t2))) (ex_intro2 T (\lambda (t2:
526 T).((eq T (THead (Flat Cast) t t0) t2) \to (\forall (P: Prop).P))) (\lambda
527 (t2: T).(pr0 (THead (Flat Cast) t t0) t2)) t0 (\lambda (H1: (eq T (THead
528 (Flat Cast) t t0) t0)).(\lambda (P: Prop).(thead_x_y_y (Flat Cast) t t0 H1
529 P))) (pr0_epsilon t0 t0 (pr0_refl t0) t)))])])))))) t1).