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