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