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_1/ty3/defs.ma".
19 include "basic_1/pc3/props.ma".
21 implied rec lemma ty3_ind (g: G) (P: (C \to (T \to (T \to Prop)))) (f:
22 (\forall (c: C).(\forall (t2: T).(\forall (t: T).((ty3 g c t2 t) \to ((P c t2
23 t) \to (\forall (u: T).(\forall (t1: T).((ty3 g c u t1) \to ((P c u t1) \to
24 ((pc3 c t1 t2) \to (P c u t2)))))))))))) (f0: (\forall (c: C).(\forall (m:
25 nat).(P c (TSort m) (TSort (next g m)))))) (f1: (\forall (n: nat).(\forall
26 (c: C).(\forall (d: C).(\forall (u: T).((getl n c (CHead d (Bind Abbr) u))
27 \to (\forall (t: T).((ty3 g d u t) \to ((P d u t) \to (P c (TLRef n) (lift (S
28 n) O t))))))))))) (f2: (\forall (n: nat).(\forall (c: C).(\forall (d:
29 C).(\forall (u: T).((getl n c (CHead d (Bind Abst) u)) \to (\forall (t:
30 T).((ty3 g d u t) \to ((P d u t) \to (P c (TLRef n) (lift (S n) O
31 u))))))))))) (f3: (\forall (c: C).(\forall (u: T).(\forall (t: T).((ty3 g c u
32 t) \to ((P c u t) \to (\forall (b: B).(\forall (t1: T).(\forall (t2: T).((ty3
33 g (CHead c (Bind b) u) t1 t2) \to ((P (CHead c (Bind b) u) t1 t2) \to (P c
34 (THead (Bind b) u t1) (THead (Bind b) u t2))))))))))))) (f4: (\forall (c:
35 C).(\forall (w: T).(\forall (u: T).((ty3 g c w u) \to ((P c w u) \to (\forall
36 (v: T).(\forall (t: T).((ty3 g c v (THead (Bind Abst) u t)) \to ((P c v
37 (THead (Bind Abst) u t)) \to (P c (THead (Flat Appl) w v) (THead (Flat Appl)
38 w (THead (Bind Abst) u t))))))))))))) (f5: (\forall (c: C).(\forall (t1:
39 T).(\forall (t2: T).((ty3 g c t1 t2) \to ((P c t1 t2) \to (\forall (t0:
40 T).((ty3 g c t2 t0) \to ((P c t2 t0) \to (P c (THead (Flat Cast) t2 t1)
41 (THead (Flat Cast) t0 t2))))))))))) (c: C) (t: T) (t0: T) (t1: ty3 g c t t0)
42 on t1: P c t t0 \def match t1 with [(ty3_conv c0 t2 t3 t4 u t5 t6 p)
43 \Rightarrow (f c0 t2 t3 t4 ((ty3_ind g P f f0 f1 f2 f3 f4 f5) c0 t2 t3 t4) u
44 t5 t6 ((ty3_ind g P f f0 f1 f2 f3 f4 f5) c0 u t5 t6) p) | (ty3_sort c0 m)
45 \Rightarrow (f0 c0 m) | (ty3_abbr n c0 d u g0 t2 t3) \Rightarrow (f1 n c0 d u
46 g0 t2 t3 ((ty3_ind g P f f0 f1 f2 f3 f4 f5) d u t2 t3)) | (ty3_abst n c0 d u
47 g0 t2 t3) \Rightarrow (f2 n c0 d u g0 t2 t3 ((ty3_ind g P f f0 f1 f2 f3 f4
48 f5) d u t2 t3)) | (ty3_bind c0 u t2 t3 b t4 t5 t6) \Rightarrow (f3 c0 u t2 t3
49 ((ty3_ind g P f f0 f1 f2 f3 f4 f5) c0 u t2 t3) b t4 t5 t6 ((ty3_ind g P f f0
50 f1 f2 f3 f4 f5) (CHead c0 (Bind b) u) t4 t5 t6)) | (ty3_appl c0 w u t2 v t3
51 t4) \Rightarrow (f4 c0 w u t2 ((ty3_ind g P f f0 f1 f2 f3 f4 f5) c0 w u t2) v
52 t3 t4 ((ty3_ind g P f f0 f1 f2 f3 f4 f5) c0 v (THead (Bind Abst) u t3) t4)) |
53 (ty3_cast c0 t2 t3 t4 t5 t6) \Rightarrow (f5 c0 t2 t3 t4 ((ty3_ind g P f f0
54 f1 f2 f3 f4 f5) c0 t2 t3 t4) t5 t6 ((ty3_ind g P f f0 f1 f2 f3 f4 f5) c0 t3
57 implied rec lemma tys3_ind (g: G) (c: C) (P: (TList \to (T \to Prop))) (f:
58 (\forall (u: T).(\forall (u0: T).((ty3 g c u u0) \to (P TNil u))))) (f0:
59 (\forall (t: T).(\forall (u: T).((ty3 g c t u) \to (\forall (ts:
60 TList).((tys3 g c ts u) \to ((P ts u) \to (P (TCons t ts) u)))))))) (t:
61 TList) (t0: T) (t1: tys3 g c t t0) on t1: P t t0 \def match t1 with
62 [(tys3_nil u u0 t2) \Rightarrow (f u u0 t2) | (tys3_cons t2 u t3 ts t4)
63 \Rightarrow (f0 t2 u t3 ts t4 ((tys3_ind g c P f f0) ts u t4))].
66 \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((ty3 g c
67 (TSort n) x) \to (pc3 c (TSort (next g n)) x)))))
69 \lambda (g: G).(\lambda (c: C).(\lambda (x: T).(\lambda (n: nat).(\lambda
70 (H: (ty3 g c (TSort n) x)).(insert_eq T (TSort n) (\lambda (t: T).(ty3 g c t
71 x)) (\lambda (_: T).(pc3 c (TSort (next g n)) x)) (\lambda (y: T).(\lambda
72 (H0: (ty3 g c y x)).(ty3_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0:
73 T).((eq T t (TSort n)) \to (pc3 c0 (TSort (next g n)) t0))))) (\lambda (c0:
74 C).(\lambda (t2: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 t2 t)).(\lambda
75 (_: (((eq T t2 (TSort n)) \to (pc3 c0 (TSort (next g n)) t)))).(\lambda (u:
76 T).(\lambda (t1: T).(\lambda (H3: (ty3 g c0 u t1)).(\lambda (H4: (((eq T u
77 (TSort n)) \to (pc3 c0 (TSort (next g n)) t1)))).(\lambda (H5: (pc3 c0 t1
78 t2)).(\lambda (H6: (eq T u (TSort n))).(let H7 \def (f_equal T T (\lambda (e:
79 T).e) u (TSort n) H6) in (let H8 \def (eq_ind T u (\lambda (t0: T).((eq T t0
80 (TSort n)) \to (pc3 c0 (TSort (next g n)) t1))) H4 (TSort n) H7) in (let H9
81 \def (eq_ind T u (\lambda (t0: T).(ty3 g c0 t0 t1)) H3 (TSort n) H7) in
82 (pc3_t t1 c0 (TSort (next g n)) (H8 (refl_equal T (TSort n))) t2
83 H5))))))))))))))) (\lambda (c0: C).(\lambda (m: nat).(\lambda (H1: (eq T
84 (TSort m) (TSort n))).(let H2 \def (f_equal T nat (\lambda (e: T).(match e
85 with [(TSort n0) \Rightarrow n0 | (TLRef _) \Rightarrow m | (THead _ _ _)
86 \Rightarrow m])) (TSort m) (TSort n) H1) in (eq_ind_r nat n (\lambda (n0:
87 nat).(pc3 c0 (TSort (next g n)) (TSort (next g n0)))) (pc3_refl c0 (TSort
88 (next g n))) m H2))))) (\lambda (n0: nat).(\lambda (c0: C).(\lambda (d:
89 C).(\lambda (u: T).(\lambda (_: (getl n0 c0 (CHead d (Bind Abbr)
90 u))).(\lambda (t: T).(\lambda (_: (ty3 g d u t)).(\lambda (_: (((eq T u
91 (TSort n)) \to (pc3 d (TSort (next g n)) t)))).(\lambda (H4: (eq T (TLRef n0)
92 (TSort n))).(let H5 \def (eq_ind T (TLRef n0) (\lambda (ee: T).(match ee with
93 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _)
94 \Rightarrow False])) I (TSort n) H4) in (False_ind (pc3 c0 (TSort (next g n))
95 (lift (S n0) O t)) H5))))))))))) (\lambda (n0: nat).(\lambda (c0: C).(\lambda
96 (d: C).(\lambda (u: T).(\lambda (_: (getl n0 c0 (CHead d (Bind Abst)
97 u))).(\lambda (t: T).(\lambda (_: (ty3 g d u t)).(\lambda (_: (((eq T u
98 (TSort n)) \to (pc3 d (TSort (next g n)) t)))).(\lambda (H4: (eq T (TLRef n0)
99 (TSort n))).(let H5 \def (eq_ind T (TLRef n0) (\lambda (ee: T).(match ee with
100 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _)
101 \Rightarrow False])) I (TSort n) H4) in (False_ind (pc3 c0 (TSort (next g n))
102 (lift (S n0) O u)) H5))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda
103 (t: T).(\lambda (_: (ty3 g c0 u t)).(\lambda (_: (((eq T u (TSort n)) \to
104 (pc3 c0 (TSort (next g n)) t)))).(\lambda (b: B).(\lambda (t1: T).(\lambda
105 (t2: T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t1 t2)).(\lambda (_: (((eq
106 T t1 (TSort n)) \to (pc3 (CHead c0 (Bind b) u) (TSort (next g n))
107 t2)))).(\lambda (H5: (eq T (THead (Bind b) u t1) (TSort n))).(let H6 \def
108 (eq_ind T (THead (Bind b) u t1) (\lambda (ee: T).(match ee with [(TSort _)
109 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
110 True])) I (TSort n) H5) in (False_ind (pc3 c0 (TSort (next g n)) (THead (Bind
111 b) u t2)) H6))))))))))))) (\lambda (c0: C).(\lambda (w: T).(\lambda (u:
112 T).(\lambda (_: (ty3 g c0 w u)).(\lambda (_: (((eq T w (TSort n)) \to (pc3 c0
113 (TSort (next g n)) u)))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g
114 c0 v (THead (Bind Abst) u t))).(\lambda (_: (((eq T v (TSort n)) \to (pc3 c0
115 (TSort (next g n)) (THead (Bind Abst) u t))))).(\lambda (H5: (eq T (THead
116 (Flat Appl) w v) (TSort n))).(let H6 \def (eq_ind T (THead (Flat Appl) w v)
117 (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
118 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H5) in
119 (False_ind (pc3 c0 (TSort (next g n)) (THead (Flat Appl) w (THead (Bind Abst)
120 u t))) H6)))))))))))) (\lambda (c0: C).(\lambda (t1: T).(\lambda (t2:
121 T).(\lambda (_: (ty3 g c0 t1 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (pc3
122 c0 (TSort (next g n)) t2)))).(\lambda (t0: T).(\lambda (_: (ty3 g c0 t2
123 t0)).(\lambda (_: (((eq T t2 (TSort n)) \to (pc3 c0 (TSort (next g n))
124 t0)))).(\lambda (H5: (eq T (THead (Flat Cast) t2 t1) (TSort n))).(let H6 \def
125 (eq_ind T (THead (Flat Cast) t2 t1) (\lambda (ee: T).(match ee with [(TSort
126 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
127 \Rightarrow True])) I (TSort n) H5) in (False_ind (pc3 c0 (TSort (next g n))
128 (THead (Flat Cast) t0 t2)) H6))))))))))) c y x H0))) H))))).
131 \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((ty3 g c
132 (TLRef n) x) \to (or (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda
133 (t: T).(pc3 c (lift (S n) O t) x)))) (\lambda (e: C).(\lambda (u: T).(\lambda
134 (_: T).(getl n c (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
135 T).(\lambda (t: T).(ty3 g e u t))))) (ex3_3 C T T (\lambda (_: C).(\lambda
136 (u: T).(\lambda (_: T).(pc3 c (lift (S n) O u) x)))) (\lambda (e: C).(\lambda
137 (u: T).(\lambda (_: T).(getl n c (CHead e (Bind Abst) u))))) (\lambda (e:
138 C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t))))))))))
140 \lambda (g: G).(\lambda (c: C).(\lambda (x: T).(\lambda (n: nat).(\lambda
141 (H: (ty3 g c (TLRef n) x)).(insert_eq T (TLRef n) (\lambda (t: T).(ty3 g c t
142 x)) (\lambda (_: T).(or (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda
143 (t0: T).(pc3 c (lift (S n) O t0) x)))) (\lambda (e: C).(\lambda (u:
144 T).(\lambda (_: T).(getl n c (CHead e (Bind Abbr) u))))) (\lambda (e:
145 C).(\lambda (u: T).(\lambda (t0: T).(ty3 g e u t0))))) (ex3_3 C T T (\lambda
146 (_: C).(\lambda (u: T).(\lambda (_: T).(pc3 c (lift (S n) O u) x)))) (\lambda
147 (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c (CHead e (Bind Abst) u)))))
148 (\lambda (e: C).(\lambda (u: T).(\lambda (t0: T).(ty3 g e u t0)))))))
149 (\lambda (y: T).(\lambda (H0: (ty3 g c y x)).(ty3_ind g (\lambda (c0:
150 C).(\lambda (t: T).(\lambda (t0: T).((eq T t (TLRef n)) \to (or (ex3_3 C T T
151 (\lambda (_: C).(\lambda (_: T).(\lambda (t1: T).(pc3 c0 (lift (S n) O t1)
152 t0)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e
153 (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t1: T).(ty3 g e
154 u t1))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(pc3
155 c0 (lift (S n) O u) t0)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_:
156 T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u:
157 T).(\lambda (t1: T).(ty3 g e u t1)))))))))) (\lambda (c0: C).(\lambda (t2:
158 T).(\lambda (t: T).(\lambda (_: (ty3 g c0 t2 t)).(\lambda (_: (((eq T t2
159 (TLRef n)) \to (or (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0:
160 T).(pc3 c0 (lift (S n) O t0) t)))) (\lambda (e: C).(\lambda (u: T).(\lambda
161 (_: T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
162 T).(\lambda (t0: T).(ty3 g e u t0))))) (ex3_3 C T T (\lambda (_: C).(\lambda
163 (u: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u) t)))) (\lambda (e:
164 C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u)))))
165 (\lambda (e: C).(\lambda (u: T).(\lambda (t0: T).(ty3 g e u
166 t0))))))))).(\lambda (u: T).(\lambda (t1: T).(\lambda (H3: (ty3 g c0 u
167 t1)).(\lambda (H4: (((eq T u (TLRef n)) \to (or (ex3_3 C T T (\lambda (_:
168 C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t1)))) (\lambda
169 (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr)
170 u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0)))))
171 (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 c0 (lift
172 (S n) O u0) t1)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n
173 c0 (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
174 (t0: T).(ty3 g e u0 t0))))))))).(\lambda (H5: (pc3 c0 t1 t2)).(\lambda (H6:
175 (eq T u (TLRef n))).(let H7 \def (f_equal T T (\lambda (e: T).e) u (TLRef n)
176 H6) in (let H8 \def (eq_ind T u (\lambda (t0: T).((eq T t0 (TLRef n)) \to (or
177 (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t3: T).(pc3 c0 (lift
178 (S n) O t3) t1)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n
179 c0 (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
180 (t3: T).(ty3 g e u0 t3))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u0:
181 T).(\lambda (_: T).(pc3 c0 (lift (S n) O u0) t1)))) (\lambda (e: C).(\lambda
182 (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u0))))) (\lambda (e:
183 C).(\lambda (u0: T).(\lambda (t3: T).(ty3 g e u0 t3)))))))) H4 (TLRef n) H7)
184 in (let H9 \def (eq_ind T u (\lambda (t0: T).(ty3 g c0 t0 t1)) H3 (TLRef n)
185 H7) in (let H10 \def (H8 (refl_equal T (TLRef n))) in (or_ind (ex3_3 C T T
186 (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0)
187 t1)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e
188 (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g
189 e u0 t0))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_:
190 T).(pc3 c0 (lift (S n) O u0) t1)))) (\lambda (e: C).(\lambda (u0: T).(\lambda
191 (_: T).(getl n c0 (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0:
192 T).(\lambda (t0: T).(ty3 g e u0 t0))))) (or (ex3_3 C T T (\lambda (_:
193 C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda
194 (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr)
195 u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0)))))
196 (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 c0 (lift
197 (S n) O u0) t2)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n
198 c0 (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
199 (t0: T).(ty3 g e u0 t0)))))) (\lambda (H11: (ex3_3 C T T (\lambda (_:
200 C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t1)))) (\lambda
201 (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr)
202 u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0
203 t0)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0:
204 T).(pc3 c0 (lift (S n) O t0) t1)))) (\lambda (e: C).(\lambda (u0: T).(\lambda
205 (_: T).(getl n c0 (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0:
206 T).(\lambda (t0: T).(ty3 g e u0 t0)))) (or (ex3_3 C T T (\lambda (_:
207 C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda
208 (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr)
209 u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0)))))
210 (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 c0 (lift
211 (S n) O u0) t2)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n
212 c0 (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
213 (t0: T).(ty3 g e u0 t0)))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2:
214 T).(\lambda (H12: (pc3 c0 (lift (S n) O x2) t1)).(\lambda (H13: (getl n c0
215 (CHead x0 (Bind Abbr) x1))).(\lambda (H14: (ty3 g x0 x1 x2)).(or_introl
216 (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift
217 (S n) O t0) t2)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n
218 c0 (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
219 (t0: T).(ty3 g e u0 t0))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u0:
220 T).(\lambda (_: T).(pc3 c0 (lift (S n) O u0) t2)))) (\lambda (e: C).(\lambda
221 (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u0))))) (\lambda (e:
222 C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0))))) (ex3_3_intro C T T
223 (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0)
224 t2)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e
225 (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g
226 e u0 t0)))) x0 x1 x2 (pc3_t t1 c0 (lift (S n) O x2) H12 t2 H5) H13
227 H14)))))))) H11)) (\lambda (H11: (ex3_3 C T T (\lambda (_: C).(\lambda (u0:
228 T).(\lambda (_: T).(pc3 c0 (lift (S n) O u0) t1)))) (\lambda (e: C).(\lambda
229 (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u0))))) (\lambda (e:
230 C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0)))))).(ex3_3_ind C T T
231 (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u0)
232 t1)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e
233 (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g
234 e u0 t0)))) (or (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0:
235 T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda (e: C).(\lambda (u0: T).(\lambda
236 (_: T).(getl n c0 (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0:
237 T).(\lambda (t0: T).(ty3 g e u0 t0))))) (ex3_3 C T T (\lambda (_: C).(\lambda
238 (u0: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u0) t2)))) (\lambda (e:
239 C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u0)))))
240 (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0))))))
241 (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: T).(\lambda (H12: (pc3 c0
242 (lift (S n) O x1) t1)).(\lambda (H13: (getl n c0 (CHead x0 (Bind Abst)
243 x1))).(\lambda (H14: (ty3 g x0 x1 x2)).(or_intror (ex3_3 C T T (\lambda (_:
244 C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda
245 (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr)
246 u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0)))))
247 (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 c0 (lift
248 (S n) O u0) t2)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n
249 c0 (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
250 (t0: T).(ty3 g e u0 t0))))) (ex3_3_intro C T T (\lambda (_: C).(\lambda (u0:
251 T).(\lambda (_: T).(pc3 c0 (lift (S n) O u0) t2)))) (\lambda (e: C).(\lambda
252 (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u0))))) (\lambda (e:
253 C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0)))) x0 x1 x2 (pc3_t t1 c0
254 (lift (S n) O x1) H12 t2 H5) H13 H14)))))))) H11)) H10))))))))))))))))
255 (\lambda (c0: C).(\lambda (m: nat).(\lambda (H1: (eq T (TSort m) (TLRef
256 n))).(let H2 \def (eq_ind T (TSort m) (\lambda (ee: T).(match ee with [(TSort
257 _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
258 False])) I (TLRef n) H1) in (False_ind (or (ex3_3 C T T (\lambda (_:
259 C).(\lambda (_: T).(\lambda (t: T).(pc3 c0 (lift (S n) O t) (TSort (next g
260 m)))))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e
261 (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u
262 t))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(pc3 c0
263 (lift (S n) O u) (TSort (next g m)))))) (\lambda (e: C).(\lambda (u:
264 T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e:
265 C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t)))))) H2))))) (\lambda (n0:
266 nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (H1: (getl n0
267 c0 (CHead d (Bind Abbr) u))).(\lambda (t: T).(\lambda (H2: (ty3 g d u
268 t)).(\lambda (_: (((eq T u (TLRef n)) \to (or (ex3_3 C T T (\lambda (_:
269 C).(\lambda (_: T).(\lambda (t0: T).(pc3 d (lift (S n) O t0) t)))) (\lambda
270 (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n d (CHead e (Bind Abbr)
271 u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0)))))
272 (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 d (lift (S
273 n) O u0) t)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n d
274 (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0:
275 T).(ty3 g e u0 t0))))))))).(\lambda (H4: (eq T (TLRef n0) (TLRef n))).(let H5
276 \def (f_equal T nat (\lambda (e: T).(match e with [(TSort _) \Rightarrow n0 |
277 (TLRef n1) \Rightarrow n1 | (THead _ _ _) \Rightarrow n0])) (TLRef n0) (TLRef
278 n) H4) in (let H6 \def (eq_ind nat n0 (\lambda (n1: nat).(getl n1 c0 (CHead d
279 (Bind Abbr) u))) H1 n H5) in (eq_ind_r nat n (\lambda (n1: nat).(or (ex3_3 C
280 T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O
281 t0) (lift (S n1) O t))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
282 T).(getl n c0 (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0:
283 T).(\lambda (t0: T).(ty3 g e u0 t0))))) (ex3_3 C T T (\lambda (_: C).(\lambda
284 (u0: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u0) (lift (S n1) O t)))))
285 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
286 Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0
287 t0))))))) (or_introl (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda
288 (t0: T).(pc3 c0 (lift (S n) O t0) (lift (S n) O t))))) (\lambda (e:
289 C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u0)))))
290 (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0))))) (ex3_3
291 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 c0 (lift (S n) O
292 u0) (lift (S n) O t))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
293 T).(getl n c0 (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0:
294 T).(\lambda (t0: T).(ty3 g e u0 t0))))) (ex3_3_intro C T T (\lambda (_:
295 C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) (lift (S n) O
296 t))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e
297 (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g
298 e u0 t0)))) d u t (pc3_refl c0 (lift (S n) O t)) H6 H2)) n0 H5))))))))))))
299 (\lambda (n0: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda
300 (H1: (getl n0 c0 (CHead d (Bind Abst) u))).(\lambda (t: T).(\lambda (H2: (ty3
301 g d u t)).(\lambda (_: (((eq T u (TLRef n)) \to (or (ex3_3 C T T (\lambda (_:
302 C).(\lambda (_: T).(\lambda (t0: T).(pc3 d (lift (S n) O t0) t)))) (\lambda
303 (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n d (CHead e (Bind Abbr)
304 u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0)))))
305 (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 d (lift (S
306 n) O u0) t)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n d
307 (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0:
308 T).(ty3 g e u0 t0))))))))).(\lambda (H4: (eq T (TLRef n0) (TLRef n))).(let H5
309 \def (f_equal T nat (\lambda (e: T).(match e with [(TSort _) \Rightarrow n0 |
310 (TLRef n1) \Rightarrow n1 | (THead _ _ _) \Rightarrow n0])) (TLRef n0) (TLRef
311 n) H4) in (let H6 \def (eq_ind nat n0 (\lambda (n1: nat).(getl n1 c0 (CHead d
312 (Bind Abst) u))) H1 n H5) in (eq_ind_r nat n (\lambda (n1: nat).(or (ex3_3 C
313 T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O
314 t0) (lift (S n1) O u))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
315 T).(getl n c0 (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0:
316 T).(\lambda (t0: T).(ty3 g e u0 t0))))) (ex3_3 C T T (\lambda (_: C).(\lambda
317 (u0: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u0) (lift (S n1) O u)))))
318 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
319 Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0
320 t0))))))) (or_intror (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda
321 (t0: T).(pc3 c0 (lift (S n) O t0) (lift (S n) O u))))) (\lambda (e:
322 C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u0)))))
323 (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0))))) (ex3_3
324 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 c0 (lift (S n) O
325 u0) (lift (S n) O u))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
326 T).(getl n c0 (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0:
327 T).(\lambda (t0: T).(ty3 g e u0 t0))))) (ex3_3_intro C T T (\lambda (_:
328 C).(\lambda (u0: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u0) (lift (S n) O
329 u))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e
330 (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g
331 e u0 t0)))) d u t (pc3_refl c0 (lift (S n) O u)) H6 H2)) n0 H5))))))))))))
332 (\lambda (c0: C).(\lambda (u: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 u
333 t)).(\lambda (_: (((eq T u (TLRef n)) \to (or (ex3_3 C T T (\lambda (_:
334 C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t)))) (\lambda
335 (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr)
336 u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0)))))
337 (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 c0 (lift
338 (S n) O u0) t)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0
339 (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0:
340 T).(ty3 g e u0 t0))))))))).(\lambda (b: B).(\lambda (t1: T).(\lambda (t2:
341 T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t1 t2)).(\lambda (_: (((eq T t1
342 (TLRef n)) \to (or (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0:
343 T).(pc3 (CHead c0 (Bind b) u) (lift (S n) O t0) t2)))) (\lambda (e:
344 C).(\lambda (u0: T).(\lambda (_: T).(getl n (CHead c0 (Bind b) u) (CHead e
345 (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g
346 e u0 t0))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_:
347 T).(pc3 (CHead c0 (Bind b) u) (lift (S n) O u0) t2)))) (\lambda (e:
348 C).(\lambda (u0: T).(\lambda (_: T).(getl n (CHead c0 (Bind b) u) (CHead e
349 (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g
350 e u0 t0))))))))).(\lambda (H5: (eq T (THead (Bind b) u t1) (TLRef n))).(let
351 H6 \def (eq_ind T (THead (Bind b) u t1) (\lambda (ee: T).(match ee with
352 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
353 \Rightarrow True])) I (TLRef n) H5) in (False_ind (or (ex3_3 C T T (\lambda
354 (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) (THead
355 (Bind b) u t2))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n
356 c0 (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda
357 (t0: T).(ty3 g e u0 t0))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u0:
358 T).(\lambda (_: T).(pc3 c0 (lift (S n) O u0) (THead (Bind b) u t2)))))
359 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
360 Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0
361 t0)))))) H6))))))))))))) (\lambda (c0: C).(\lambda (w: T).(\lambda (u:
362 T).(\lambda (_: (ty3 g c0 w u)).(\lambda (_: (((eq T w (TLRef n)) \to (or
363 (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 c0 (lift (S
364 n) O t) u)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0
365 (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t:
366 T).(ty3 g e u0 t))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda
367 (_: T).(pc3 c0 (lift (S n) O u0) u)))) (\lambda (e: C).(\lambda (u0:
368 T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u0))))) (\lambda (e:
369 C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))))))).(\lambda (v:
370 T).(\lambda (t: T).(\lambda (_: (ty3 g c0 v (THead (Bind Abst) u
371 t))).(\lambda (_: (((eq T v (TLRef n)) \to (or (ex3_3 C T T (\lambda (_:
372 C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) (THead (Bind
373 Abst) u t))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0
374 (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0:
375 T).(ty3 g e u0 t0))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda
376 (_: T).(pc3 c0 (lift (S n) O u0) (THead (Bind Abst) u t))))) (\lambda (e:
377 C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u0)))))
378 (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0
379 t0))))))))).(\lambda (H5: (eq T (THead (Flat Appl) w v) (TLRef n))).(let H6
380 \def (eq_ind T (THead (Flat Appl) w v) (\lambda (ee: T).(match ee with
381 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
382 \Rightarrow True])) I (TLRef n) H5) in (False_ind (or (ex3_3 C T T (\lambda
383 (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) (THead
384 (Flat Appl) w (THead (Bind Abst) u t)))))) (\lambda (e: C).(\lambda (u0:
385 T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u0))))) (\lambda (e:
386 C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0))))) (ex3_3 C T T
387 (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u0)
388 (THead (Flat Appl) w (THead (Bind Abst) u t)))))) (\lambda (e: C).(\lambda
389 (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u0))))) (\lambda (e:
390 C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0 t0)))))) H6))))))))))))
391 (\lambda (c0: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g c0 t1
392 t2)).(\lambda (_: (((eq T t1 (TLRef n)) \to (or (ex3_3 C T T (\lambda (_:
393 C).(\lambda (_: T).(\lambda (t: T).(pc3 c0 (lift (S n) O t) t2)))) (\lambda
394 (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u)))))
395 (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t))))) (ex3_3 C T
396 T (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u)
397 t2)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e
398 (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u
399 t))))))))).(\lambda (t0: T).(\lambda (_: (ty3 g c0 t2 t0)).(\lambda (_: (((eq
400 T t2 (TLRef n)) \to (or (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda
401 (t: T).(pc3 c0 (lift (S n) O t) t0)))) (\lambda (e: C).(\lambda (u:
402 T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e:
403 C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t))))) (ex3_3 C T T (\lambda
404 (_: C).(\lambda (u: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u) t0))))
405 (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
406 Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u
407 t))))))))).(\lambda (H5: (eq T (THead (Flat Cast) t2 t1) (TLRef n))).(let H6
408 \def (eq_ind T (THead (Flat Cast) t2 t1) (\lambda (ee: T).(match ee with
409 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
410 \Rightarrow True])) I (TLRef n) H5) in (False_ind (or (ex3_3 C T T (\lambda
411 (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 c0 (lift (S n) O t) (THead (Flat
412 Cast) t0 t2))))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0
413 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t:
414 T).(ty3 g e u t))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u: T).(\lambda
415 (_: T).(pc3 c0 (lift (S n) O u) (THead (Flat Cast) t0 t2))))) (\lambda (e:
416 C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u)))))
417 (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t))))))
418 H6))))))))))) c y x H0))) H))))).
421 \forall (g: G).(\forall (b: B).(\forall (c: C).(\forall (u: T).(\forall (t1:
422 T).(\forall (x: T).((ty3 g c (THead (Bind b) u t1) x) \to (ex3_2 T T (\lambda
423 (t2: T).(\lambda (_: T).(pc3 c (THead (Bind b) u t2) x))) (\lambda (_:
424 T).(\lambda (t: T).(ty3 g c u t))) (\lambda (t2: T).(\lambda (_: T).(ty3 g
425 (CHead c (Bind b) u) t1 t2))))))))))
427 \lambda (g: G).(\lambda (b: B).(\lambda (c: C).(\lambda (u: T).(\lambda (t1:
428 T).(\lambda (x: T).(\lambda (H: (ty3 g c (THead (Bind b) u t1) x)).(insert_eq
429 T (THead (Bind b) u t1) (\lambda (t: T).(ty3 g c t x)) (\lambda (_: T).(ex3_2
430 T T (\lambda (t2: T).(\lambda (_: T).(pc3 c (THead (Bind b) u t2) x)))
431 (\lambda (_: T).(\lambda (t0: T).(ty3 g c u t0))) (\lambda (t2: T).(\lambda
432 (_: T).(ty3 g (CHead c (Bind b) u) t1 t2))))) (\lambda (y: T).(\lambda (H0:
433 (ty3 g c y x)).(ty3_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0:
434 T).((eq T t (THead (Bind b) u t1)) \to (ex3_2 T T (\lambda (t2: T).(\lambda
435 (_: T).(pc3 c0 (THead (Bind b) u t2) t0))) (\lambda (_: T).(\lambda (t3:
436 T).(ty3 g c0 u t3))) (\lambda (t2: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind
437 b) u) t1 t2)))))))) (\lambda (c0: C).(\lambda (t2: T).(\lambda (t:
438 T).(\lambda (_: (ty3 g c0 t2 t)).(\lambda (_: (((eq T t2 (THead (Bind b) u
439 t1)) \to (ex3_2 T T (\lambda (t3: T).(\lambda (_: T).(pc3 c0 (THead (Bind b)
440 u t3) t))) (\lambda (_: T).(\lambda (t0: T).(ty3 g c0 u t0))) (\lambda (t3:
441 T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t3))))))).(\lambda (u0:
442 T).(\lambda (t0: T).(\lambda (H3: (ty3 g c0 u0 t0)).(\lambda (H4: (((eq T u0
443 (THead (Bind b) u t1)) \to (ex3_2 T T (\lambda (t3: T).(\lambda (_: T).(pc3
444 c0 (THead (Bind b) u t3) t0))) (\lambda (_: T).(\lambda (t4: T).(ty3 g c0 u
445 t4))) (\lambda (t3: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1
446 t3))))))).(\lambda (H5: (pc3 c0 t0 t2)).(\lambda (H6: (eq T u0 (THead (Bind
447 b) u t1))).(let H7 \def (f_equal T T (\lambda (e: T).e) u0 (THead (Bind b) u
448 t1) H6) in (let H8 \def (eq_ind T u0 (\lambda (t3: T).((eq T t3 (THead (Bind
449 b) u t1)) \to (ex3_2 T T (\lambda (t4: T).(\lambda (_: T).(pc3 c0 (THead
450 (Bind b) u t4) t0))) (\lambda (_: T).(\lambda (t5: T).(ty3 g c0 u t5)))
451 (\lambda (t4: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t4)))))) H4
452 (THead (Bind b) u t1) H7) in (let H9 \def (eq_ind T u0 (\lambda (t3: T).(ty3
453 g c0 t3 t0)) H3 (THead (Bind b) u t1) H7) in (let H10 \def (H8 (refl_equal T
454 (THead (Bind b) u t1))) in (ex3_2_ind T T (\lambda (t3: T).(\lambda (_:
455 T).(pc3 c0 (THead (Bind b) u t3) t0))) (\lambda (_: T).(\lambda (t4: T).(ty3
456 g c0 u t4))) (\lambda (t3: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1
457 t3))) (ex3_2 T T (\lambda (t3: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u
458 t3) t2))) (\lambda (_: T).(\lambda (t4: T).(ty3 g c0 u t4))) (\lambda (t3:
459 T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t3)))) (\lambda (x0:
460 T).(\lambda (x1: T).(\lambda (H11: (pc3 c0 (THead (Bind b) u x0)
461 t0)).(\lambda (H12: (ty3 g c0 u x1)).(\lambda (H13: (ty3 g (CHead c0 (Bind b)
462 u) t1 x0)).(ex3_2_intro T T (\lambda (t3: T).(\lambda (_: T).(pc3 c0 (THead
463 (Bind b) u t3) t2))) (\lambda (_: T).(\lambda (t4: T).(ty3 g c0 u t4)))
464 (\lambda (t3: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t3))) x0 x1
465 (pc3_t t0 c0 (THead (Bind b) u x0) H11 t2 H5) H12 H13))))))
466 H10)))))))))))))))) (\lambda (c0: C).(\lambda (m: nat).(\lambda (H1: (eq T
467 (TSort m) (THead (Bind b) u t1))).(let H2 \def (eq_ind T (TSort m) (\lambda
468 (ee: T).(match ee with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow
469 False | (THead _ _ _) \Rightarrow False])) I (THead (Bind b) u t1) H1) in
470 (False_ind (ex3_2 T T (\lambda (t2: T).(\lambda (_: T).(pc3 c0 (THead (Bind
471 b) u t2) (TSort (next g m))))) (\lambda (_: T).(\lambda (t: T).(ty3 g c0 u
472 t))) (\lambda (t2: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t2))))
473 H2))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u0:
474 T).(\lambda (_: (getl n c0 (CHead d (Bind Abbr) u0))).(\lambda (t:
475 T).(\lambda (_: (ty3 g d u0 t)).(\lambda (_: (((eq T u0 (THead (Bind b) u
476 t1)) \to (ex3_2 T T (\lambda (t2: T).(\lambda (_: T).(pc3 d (THead (Bind b) u
477 t2) t))) (\lambda (_: T).(\lambda (t0: T).(ty3 g d u t0))) (\lambda (t2:
478 T).(\lambda (_: T).(ty3 g (CHead d (Bind b) u) t1 t2))))))).(\lambda (H4: (eq
479 T (TLRef n) (THead (Bind b) u t1))).(let H5 \def (eq_ind T (TLRef n) (\lambda
480 (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow
481 True | (THead _ _ _) \Rightarrow False])) I (THead (Bind b) u t1) H4) in
482 (False_ind (ex3_2 T T (\lambda (t2: T).(\lambda (_: T).(pc3 c0 (THead (Bind
483 b) u t2) (lift (S n) O t)))) (\lambda (_: T).(\lambda (t0: T).(ty3 g c0 u
484 t0))) (\lambda (t2: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t2))))
485 H5))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda
486 (u0: T).(\lambda (_: (getl n c0 (CHead d (Bind Abst) u0))).(\lambda (t:
487 T).(\lambda (_: (ty3 g d u0 t)).(\lambda (_: (((eq T u0 (THead (Bind b) u
488 t1)) \to (ex3_2 T T (\lambda (t2: T).(\lambda (_: T).(pc3 d (THead (Bind b) u
489 t2) t))) (\lambda (_: T).(\lambda (t0: T).(ty3 g d u t0))) (\lambda (t2:
490 T).(\lambda (_: T).(ty3 g (CHead d (Bind b) u) t1 t2))))))).(\lambda (H4: (eq
491 T (TLRef n) (THead (Bind b) u t1))).(let H5 \def (eq_ind T (TLRef n) (\lambda
492 (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow
493 True | (THead _ _ _) \Rightarrow False])) I (THead (Bind b) u t1) H4) in
494 (False_ind (ex3_2 T T (\lambda (t2: T).(\lambda (_: T).(pc3 c0 (THead (Bind
495 b) u t2) (lift (S n) O u0)))) (\lambda (_: T).(\lambda (t0: T).(ty3 g c0 u
496 t0))) (\lambda (t2: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t2))))
497 H5))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda (t: T).(\lambda (H1:
498 (ty3 g c0 u0 t)).(\lambda (H2: (((eq T u0 (THead (Bind b) u t1)) \to (ex3_2 T
499 T (\lambda (t2: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t2) t)))
500 (\lambda (_: T).(\lambda (t0: T).(ty3 g c0 u t0))) (\lambda (t2: T).(\lambda
501 (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t2))))))).(\lambda (b0: B).(\lambda
502 (t0: T).(\lambda (t2: T).(\lambda (H3: (ty3 g (CHead c0 (Bind b0) u0) t0
503 t2)).(\lambda (H4: (((eq T t0 (THead (Bind b) u t1)) \to (ex3_2 T T (\lambda
504 (t3: T).(\lambda (_: T).(pc3 (CHead c0 (Bind b0) u0) (THead (Bind b) u t3)
505 t2))) (\lambda (_: T).(\lambda (t4: T).(ty3 g (CHead c0 (Bind b0) u0) u t4)))
506 (\lambda (t3: T).(\lambda (_: T).(ty3 g (CHead (CHead c0 (Bind b0) u0) (Bind
507 b) u) t1 t3))))))).(\lambda (H5: (eq T (THead (Bind b0) u0 t0) (THead (Bind
508 b) u t1))).(let H6 \def (f_equal T B (\lambda (e: T).(match e with [(TSort _)
509 \Rightarrow b0 | (TLRef _) \Rightarrow b0 | (THead k _ _) \Rightarrow (match
510 k with [(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow b0])])) (THead (Bind
511 b0) u0 t0) (THead (Bind b) u t1) H5) in ((let H7 \def (f_equal T T (\lambda
512 (e: T).(match e with [(TSort _) \Rightarrow u0 | (TLRef _) \Rightarrow u0 |
513 (THead _ t3 _) \Rightarrow t3])) (THead (Bind b0) u0 t0) (THead (Bind b) u
514 t1) H5) in ((let H8 \def (f_equal T T (\lambda (e: T).(match e with [(TSort
515 _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t3) \Rightarrow
516 t3])) (THead (Bind b0) u0 t0) (THead (Bind b) u t1) H5) in (\lambda (H9: (eq
517 T u0 u)).(\lambda (H10: (eq B b0 b)).(let H11 \def (eq_ind T t0 (\lambda (t3:
518 T).((eq T t3 (THead (Bind b) u t1)) \to (ex3_2 T T (\lambda (t4: T).(\lambda
519 (_: T).(pc3 (CHead c0 (Bind b0) u0) (THead (Bind b) u t4) t2))) (\lambda (_:
520 T).(\lambda (t5: T).(ty3 g (CHead c0 (Bind b0) u0) u t5))) (\lambda (t4:
521 T).(\lambda (_: T).(ty3 g (CHead (CHead c0 (Bind b0) u0) (Bind b) u) t1
522 t4)))))) H4 t1 H8) in (let H12 \def (eq_ind T t0 (\lambda (t3: T).(ty3 g
523 (CHead c0 (Bind b0) u0) t3 t2)) H3 t1 H8) in (let H13 \def (eq_ind B b0
524 (\lambda (b1: B).((eq T t1 (THead (Bind b) u t1)) \to (ex3_2 T T (\lambda
525 (t3: T).(\lambda (_: T).(pc3 (CHead c0 (Bind b1) u0) (THead (Bind b) u t3)
526 t2))) (\lambda (_: T).(\lambda (t4: T).(ty3 g (CHead c0 (Bind b1) u0) u t4)))
527 (\lambda (t3: T).(\lambda (_: T).(ty3 g (CHead (CHead c0 (Bind b1) u0) (Bind
528 b) u) t1 t3)))))) H11 b H10) in (let H14 \def (eq_ind B b0 (\lambda (b1:
529 B).(ty3 g (CHead c0 (Bind b1) u0) t1 t2)) H12 b H10) in (eq_ind_r B b
530 (\lambda (b1: B).(ex3_2 T T (\lambda (t3: T).(\lambda (_: T).(pc3 c0 (THead
531 (Bind b) u t3) (THead (Bind b1) u0 t2)))) (\lambda (_: T).(\lambda (t4:
532 T).(ty3 g c0 u t4))) (\lambda (t3: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind
533 b) u) t1 t3))))) (let H15 \def (eq_ind T u0 (\lambda (t3: T).((eq T t1 (THead
534 (Bind b) u t1)) \to (ex3_2 T T (\lambda (t4: T).(\lambda (_: T).(pc3 (CHead
535 c0 (Bind b) t3) (THead (Bind b) u t4) t2))) (\lambda (_: T).(\lambda (t5:
536 T).(ty3 g (CHead c0 (Bind b) t3) u t5))) (\lambda (t4: T).(\lambda (_:
537 T).(ty3 g (CHead (CHead c0 (Bind b) t3) (Bind b) u) t1 t4)))))) H13 u H9) in
538 (let H16 \def (eq_ind T u0 (\lambda (t3: T).(ty3 g (CHead c0 (Bind b) t3) t1
539 t2)) H14 u H9) in (let H17 \def (eq_ind T u0 (\lambda (t3: T).((eq T t3
540 (THead (Bind b) u t1)) \to (ex3_2 T T (\lambda (t4: T).(\lambda (_: T).(pc3
541 c0 (THead (Bind b) u t4) t))) (\lambda (_: T).(\lambda (t5: T).(ty3 g c0 u
542 t5))) (\lambda (t4: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1
543 t4)))))) H2 u H9) in (let H18 \def (eq_ind T u0 (\lambda (t3: T).(ty3 g c0 t3
544 t)) H1 u H9) in (eq_ind_r T u (\lambda (t3: T).(ex3_2 T T (\lambda (t4:
545 T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t4) (THead (Bind b) t3 t2))))
546 (\lambda (_: T).(\lambda (t5: T).(ty3 g c0 u t5))) (\lambda (t4: T).(\lambda
547 (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t4))))) (ex3_2_intro T T (\lambda (t3:
548 T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t3) (THead (Bind b) u t2))))
549 (\lambda (_: T).(\lambda (t4: T).(ty3 g c0 u t4))) (\lambda (t3: T).(\lambda
550 (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t3))) t2 t (pc3_refl c0 (THead (Bind
551 b) u t2)) H18 H16) u0 H9))))) b0 H10)))))))) H7)) H6))))))))))))) (\lambda
552 (c0: C).(\lambda (w: T).(\lambda (u0: T).(\lambda (_: (ty3 g c0 w
553 u0)).(\lambda (_: (((eq T w (THead (Bind b) u t1)) \to (ex3_2 T T (\lambda
554 (t2: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t2) u0))) (\lambda (_:
555 T).(\lambda (t: T).(ty3 g c0 u t))) (\lambda (t2: T).(\lambda (_: T).(ty3 g
556 (CHead c0 (Bind b) u) t1 t2))))))).(\lambda (v: T).(\lambda (t: T).(\lambda
557 (_: (ty3 g c0 v (THead (Bind Abst) u0 t))).(\lambda (_: (((eq T v (THead
558 (Bind b) u t1)) \to (ex3_2 T T (\lambda (t2: T).(\lambda (_: T).(pc3 c0
559 (THead (Bind b) u t2) (THead (Bind Abst) u0 t)))) (\lambda (_: T).(\lambda
560 (t0: T).(ty3 g c0 u t0))) (\lambda (t2: T).(\lambda (_: T).(ty3 g (CHead c0
561 (Bind b) u) t1 t2))))))).(\lambda (H5: (eq T (THead (Flat Appl) w v) (THead
562 (Bind b) u t1))).(let H6 \def (eq_ind T (THead (Flat Appl) w v) (\lambda (ee:
563 T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
564 | (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat
565 _) \Rightarrow True])])) I (THead (Bind b) u t1) H5) in (False_ind (ex3_2 T T
566 (\lambda (t2: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t2) (THead (Flat
567 Appl) w (THead (Bind Abst) u0 t))))) (\lambda (_: T).(\lambda (t0: T).(ty3 g
568 c0 u t0))) (\lambda (t2: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1
569 t2)))) H6)))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t2:
570 T).(\lambda (_: (ty3 g c0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind b) u
571 t1)) \to (ex3_2 T T (\lambda (t3: T).(\lambda (_: T).(pc3 c0 (THead (Bind b)
572 u t3) t2))) (\lambda (_: T).(\lambda (t: T).(ty3 g c0 u t))) (\lambda (t3:
573 T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t3))))))).(\lambda (t3:
574 T).(\lambda (_: (ty3 g c0 t2 t3)).(\lambda (_: (((eq T t2 (THead (Bind b) u
575 t1)) \to (ex3_2 T T (\lambda (t4: T).(\lambda (_: T).(pc3 c0 (THead (Bind b)
576 u t4) t3))) (\lambda (_: T).(\lambda (t: T).(ty3 g c0 u t))) (\lambda (t4:
577 T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t4))))))).(\lambda (H5:
578 (eq T (THead (Flat Cast) t2 t0) (THead (Bind b) u t1))).(let H6 \def (eq_ind
579 T (THead (Flat Cast) t2 t0) (\lambda (ee: T).(match ee with [(TSort _)
580 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
581 (match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I
582 (THead (Bind b) u t1) H5) in (False_ind (ex3_2 T T (\lambda (t4: T).(\lambda
583 (_: T).(pc3 c0 (THead (Bind b) u t4) (THead (Flat Cast) t3 t2)))) (\lambda
584 (_: T).(\lambda (t: T).(ty3 g c0 u t))) (\lambda (t4: T).(\lambda (_: T).(ty3
585 g (CHead c0 (Bind b) u) t1 t4)))) H6))))))))))) c y x H0))) H))))))).
588 \forall (g: G).(\forall (c: C).(\forall (w: T).(\forall (v: T).(\forall (x:
589 T).((ty3 g c (THead (Flat Appl) w v) x) \to (ex3_2 T T (\lambda (u:
590 T).(\lambda (t: T).(pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x)))
591 (\lambda (u: T).(\lambda (t: T).(ty3 g c v (THead (Bind Abst) u t))))
592 (\lambda (u: T).(\lambda (_: T).(ty3 g c w u)))))))))
594 \lambda (g: G).(\lambda (c: C).(\lambda (w: T).(\lambda (v: T).(\lambda (x:
595 T).(\lambda (H: (ty3 g c (THead (Flat Appl) w v) x)).(insert_eq T (THead
596 (Flat Appl) w v) (\lambda (t: T).(ty3 g c t x)) (\lambda (_: T).(ex3_2 T T
597 (\lambda (u: T).(\lambda (t0: T).(pc3 c (THead (Flat Appl) w (THead (Bind
598 Abst) u t0)) x))) (\lambda (u: T).(\lambda (t0: T).(ty3 g c v (THead (Bind
599 Abst) u t0)))) (\lambda (u: T).(\lambda (_: T).(ty3 g c w u))))) (\lambda (y:
600 T).(\lambda (H0: (ty3 g c y x)).(ty3_ind g (\lambda (c0: C).(\lambda (t:
601 T).(\lambda (t0: T).((eq T t (THead (Flat Appl) w v)) \to (ex3_2 T T (\lambda
602 (u: T).(\lambda (t1: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u
603 t1)) t0))) (\lambda (u: T).(\lambda (t1: T).(ty3 g c0 v (THead (Bind Abst) u
604 t1)))) (\lambda (u: T).(\lambda (_: T).(ty3 g c0 w u)))))))) (\lambda (c0:
605 C).(\lambda (t2: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 t2 t)).(\lambda
606 (_: (((eq T t2 (THead (Flat Appl) w v)) \to (ex3_2 T T (\lambda (u:
607 T).(\lambda (t0: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u t0))
608 t))) (\lambda (u: T).(\lambda (t0: T).(ty3 g c0 v (THead (Bind Abst) u t0))))
609 (\lambda (u: T).(\lambda (_: T).(ty3 g c0 w u))))))).(\lambda (u: T).(\lambda
610 (t1: T).(\lambda (H3: (ty3 g c0 u t1)).(\lambda (H4: (((eq T u (THead (Flat
611 Appl) w v)) \to (ex3_2 T T (\lambda (u0: T).(\lambda (t0: T).(pc3 c0 (THead
612 (Flat Appl) w (THead (Bind Abst) u0 t0)) t1))) (\lambda (u0: T).(\lambda (t0:
613 T).(ty3 g c0 v (THead (Bind Abst) u0 t0)))) (\lambda (u0: T).(\lambda (_:
614 T).(ty3 g c0 w u0))))))).(\lambda (H5: (pc3 c0 t1 t2)).(\lambda (H6: (eq T u
615 (THead (Flat Appl) w v))).(let H7 \def (f_equal T T (\lambda (e: T).e) u
616 (THead (Flat Appl) w v) H6) in (let H8 \def (eq_ind T u (\lambda (t0: T).((eq
617 T t0 (THead (Flat Appl) w v)) \to (ex3_2 T T (\lambda (u0: T).(\lambda (t3:
618 T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t3)) t1))) (\lambda
619 (u0: T).(\lambda (t3: T).(ty3 g c0 v (THead (Bind Abst) u0 t3)))) (\lambda
620 (u0: T).(\lambda (_: T).(ty3 g c0 w u0)))))) H4 (THead (Flat Appl) w v) H7)
621 in (let H9 \def (eq_ind T u (\lambda (t0: T).(ty3 g c0 t0 t1)) H3 (THead
622 (Flat Appl) w v) H7) in (let H10 \def (H8 (refl_equal T (THead (Flat Appl) w
623 v))) in (ex3_2_ind T T (\lambda (u0: T).(\lambda (t0: T).(pc3 c0 (THead (Flat
624 Appl) w (THead (Bind Abst) u0 t0)) t1))) (\lambda (u0: T).(\lambda (t0:
625 T).(ty3 g c0 v (THead (Bind Abst) u0 t0)))) (\lambda (u0: T).(\lambda (_:
626 T).(ty3 g c0 w u0))) (ex3_2 T T (\lambda (u0: T).(\lambda (t0: T).(pc3 c0
627 (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t2))) (\lambda (u0:
628 T).(\lambda (t0: T).(ty3 g c0 v (THead (Bind Abst) u0 t0)))) (\lambda (u0:
629 T).(\lambda (_: T).(ty3 g c0 w u0)))) (\lambda (x0: T).(\lambda (x1:
630 T).(\lambda (H11: (pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) x0 x1))
631 t1)).(\lambda (H12: (ty3 g c0 v (THead (Bind Abst) x0 x1))).(\lambda (H13:
632 (ty3 g c0 w x0)).(ex3_2_intro T T (\lambda (u0: T).(\lambda (t0: T).(pc3 c0
633 (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t2))) (\lambda (u0:
634 T).(\lambda (t0: T).(ty3 g c0 v (THead (Bind Abst) u0 t0)))) (\lambda (u0:
635 T).(\lambda (_: T).(ty3 g c0 w u0))) x0 x1 (pc3_t t1 c0 (THead (Flat Appl) w
636 (THead (Bind Abst) x0 x1)) H11 t2 H5) H12 H13)))))) H10))))))))))))))))
637 (\lambda (c0: C).(\lambda (m: nat).(\lambda (H1: (eq T (TSort m) (THead (Flat
638 Appl) w v))).(let H2 \def (eq_ind T (TSort m) (\lambda (ee: T).(match ee with
639 [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _)
640 \Rightarrow False])) I (THead (Flat Appl) w v) H1) in (False_ind (ex3_2 T T
641 (\lambda (u: T).(\lambda (t: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind
642 Abst) u t)) (TSort (next g m))))) (\lambda (u: T).(\lambda (t: T).(ty3 g c0 v
643 (THead (Bind Abst) u t)))) (\lambda (u: T).(\lambda (_: T).(ty3 g c0 w u))))
644 H2))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u:
645 T).(\lambda (_: (getl n c0 (CHead d (Bind Abbr) u))).(\lambda (t: T).(\lambda
646 (_: (ty3 g d u t)).(\lambda (_: (((eq T u (THead (Flat Appl) w v)) \to (ex3_2
647 T T (\lambda (u0: T).(\lambda (t0: T).(pc3 d (THead (Flat Appl) w (THead
648 (Bind Abst) u0 t0)) t))) (\lambda (u0: T).(\lambda (t0: T).(ty3 g d v (THead
649 (Bind Abst) u0 t0)))) (\lambda (u0: T).(\lambda (_: T).(ty3 g d w
650 u0))))))).(\lambda (H4: (eq T (TLRef n) (THead (Flat Appl) w v))).(let H5
651 \def (eq_ind T (TLRef n) (\lambda (ee: T).(match ee with [(TSort _)
652 \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow
653 False])) I (THead (Flat Appl) w v) H4) in (False_ind (ex3_2 T T (\lambda (u0:
654 T).(\lambda (t0: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t0))
655 (lift (S n) O t)))) (\lambda (u0: T).(\lambda (t0: T).(ty3 g c0 v (THead
656 (Bind Abst) u0 t0)))) (\lambda (u0: T).(\lambda (_: T).(ty3 g c0 w u0))))
657 H5))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u:
658 T).(\lambda (_: (getl n c0 (CHead d (Bind Abst) u))).(\lambda (t: T).(\lambda
659 (_: (ty3 g d u t)).(\lambda (_: (((eq T u (THead (Flat Appl) w v)) \to (ex3_2
660 T T (\lambda (u0: T).(\lambda (t0: T).(pc3 d (THead (Flat Appl) w (THead
661 (Bind Abst) u0 t0)) t))) (\lambda (u0: T).(\lambda (t0: T).(ty3 g d v (THead
662 (Bind Abst) u0 t0)))) (\lambda (u0: T).(\lambda (_: T).(ty3 g d w
663 u0))))))).(\lambda (H4: (eq T (TLRef n) (THead (Flat Appl) w v))).(let H5
664 \def (eq_ind T (TLRef n) (\lambda (ee: T).(match ee with [(TSort _)
665 \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow
666 False])) I (THead (Flat Appl) w v) H4) in (False_ind (ex3_2 T T (\lambda (u0:
667 T).(\lambda (t0: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t0))
668 (lift (S n) O u)))) (\lambda (u0: T).(\lambda (t0: T).(ty3 g c0 v (THead
669 (Bind Abst) u0 t0)))) (\lambda (u0: T).(\lambda (_: T).(ty3 g c0 w u0))))
670 H5))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda (t: T).(\lambda (_:
671 (ty3 g c0 u t)).(\lambda (_: (((eq T u (THead (Flat Appl) w v)) \to (ex3_2 T
672 T (\lambda (u0: T).(\lambda (t0: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind
673 Abst) u0 t0)) t))) (\lambda (u0: T).(\lambda (t0: T).(ty3 g c0 v (THead (Bind
674 Abst) u0 t0)))) (\lambda (u0: T).(\lambda (_: T).(ty3 g c0 w
675 u0))))))).(\lambda (b: B).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (ty3
676 g (CHead c0 (Bind b) u) t1 t2)).(\lambda (_: (((eq T t1 (THead (Flat Appl) w
677 v)) \to (ex3_2 T T (\lambda (u0: T).(\lambda (t0: T).(pc3 (CHead c0 (Bind b)
678 u) (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t2))) (\lambda (u0:
679 T).(\lambda (t0: T).(ty3 g (CHead c0 (Bind b) u) v (THead (Bind Abst) u0
680 t0)))) (\lambda (u0: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) w
681 u0))))))).(\lambda (H5: (eq T (THead (Bind b) u t1) (THead (Flat Appl) w
682 v))).(let H6 \def (eq_ind T (THead (Bind b) u t1) (\lambda (ee: T).(match ee
683 with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _
684 _) \Rightarrow (match k with [(Bind _) \Rightarrow True | (Flat _)
685 \Rightarrow False])])) I (THead (Flat Appl) w v) H5) in (False_ind (ex3_2 T T
686 (\lambda (u0: T).(\lambda (t0: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind
687 Abst) u0 t0)) (THead (Bind b) u t2)))) (\lambda (u0: T).(\lambda (t0: T).(ty3
688 g c0 v (THead (Bind Abst) u0 t0)))) (\lambda (u0: T).(\lambda (_: T).(ty3 g
689 c0 w u0)))) H6))))))))))))) (\lambda (c0: C).(\lambda (w0: T).(\lambda (u:
690 T).(\lambda (H1: (ty3 g c0 w0 u)).(\lambda (H2: (((eq T w0 (THead (Flat Appl)
691 w v)) \to (ex3_2 T T (\lambda (u0: T).(\lambda (t: T).(pc3 c0 (THead (Flat
692 Appl) w (THead (Bind Abst) u0 t)) u))) (\lambda (u0: T).(\lambda (t: T).(ty3
693 g c0 v (THead (Bind Abst) u0 t)))) (\lambda (u0: T).(\lambda (_: T).(ty3 g c0
694 w u0))))))).(\lambda (v0: T).(\lambda (t: T).(\lambda (H3: (ty3 g c0 v0
695 (THead (Bind Abst) u t))).(\lambda (H4: (((eq T v0 (THead (Flat Appl) w v))
696 \to (ex3_2 T T (\lambda (u0: T).(\lambda (t0: T).(pc3 c0 (THead (Flat Appl) w
697 (THead (Bind Abst) u0 t0)) (THead (Bind Abst) u t)))) (\lambda (u0:
698 T).(\lambda (t0: T).(ty3 g c0 v (THead (Bind Abst) u0 t0)))) (\lambda (u0:
699 T).(\lambda (_: T).(ty3 g c0 w u0))))))).(\lambda (H5: (eq T (THead (Flat
700 Appl) w0 v0) (THead (Flat Appl) w v))).(let H6 \def (f_equal T T (\lambda (e:
701 T).(match e with [(TSort _) \Rightarrow w0 | (TLRef _) \Rightarrow w0 |
702 (THead _ t0 _) \Rightarrow t0])) (THead (Flat Appl) w0 v0) (THead (Flat Appl)
703 w v) H5) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e with [(TSort
704 _) \Rightarrow v0 | (TLRef _) \Rightarrow v0 | (THead _ _ t0) \Rightarrow
705 t0])) (THead (Flat Appl) w0 v0) (THead (Flat Appl) w v) H5) in (\lambda (H8:
706 (eq T w0 w)).(let H9 \def (eq_ind T v0 (\lambda (t0: T).((eq T t0 (THead
707 (Flat Appl) w v)) \to (ex3_2 T T (\lambda (u0: T).(\lambda (t1: T).(pc3 c0
708 (THead (Flat Appl) w (THead (Bind Abst) u0 t1)) (THead (Bind Abst) u t))))
709 (\lambda (u0: T).(\lambda (t1: T).(ty3 g c0 v (THead (Bind Abst) u0 t1))))
710 (\lambda (u0: T).(\lambda (_: T).(ty3 g c0 w u0)))))) H4 v H7) in (let H10
711 \def (eq_ind T v0 (\lambda (t0: T).(ty3 g c0 t0 (THead (Bind Abst) u t))) H3
712 v H7) in (let H11 \def (eq_ind T w0 (\lambda (t0: T).((eq T t0 (THead (Flat
713 Appl) w v)) \to (ex3_2 T T (\lambda (u0: T).(\lambda (t1: T).(pc3 c0 (THead
714 (Flat Appl) w (THead (Bind Abst) u0 t1)) u))) (\lambda (u0: T).(\lambda (t1:
715 T).(ty3 g c0 v (THead (Bind Abst) u0 t1)))) (\lambda (u0: T).(\lambda (_:
716 T).(ty3 g c0 w u0)))))) H2 w H8) in (let H12 \def (eq_ind T w0 (\lambda (t0:
717 T).(ty3 g c0 t0 u)) H1 w H8) in (eq_ind_r T w (\lambda (t0: T).(ex3_2 T T
718 (\lambda (u0: T).(\lambda (t1: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind
719 Abst) u0 t1)) (THead (Flat Appl) t0 (THead (Bind Abst) u t))))) (\lambda (u0:
720 T).(\lambda (t1: T).(ty3 g c0 v (THead (Bind Abst) u0 t1)))) (\lambda (u0:
721 T).(\lambda (_: T).(ty3 g c0 w u0))))) (ex3_2_intro T T (\lambda (u0:
722 T).(\lambda (t0: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t0))
723 (THead (Flat Appl) w (THead (Bind Abst) u t))))) (\lambda (u0: T).(\lambda
724 (t0: T).(ty3 g c0 v (THead (Bind Abst) u0 t0)))) (\lambda (u0: T).(\lambda
725 (_: T).(ty3 g c0 w u0))) u t (pc3_refl c0 (THead (Flat Appl) w (THead (Bind
726 Abst) u t))) H10 H12) w0 H8))))))) H6)))))))))))) (\lambda (c0: C).(\lambda
727 (t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g c0 t1 t2)).(\lambda (_: (((eq T
728 t1 (THead (Flat Appl) w v)) \to (ex3_2 T T (\lambda (u: T).(\lambda (t:
729 T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t2))) (\lambda (u:
730 T).(\lambda (t: T).(ty3 g c0 v (THead (Bind Abst) u t)))) (\lambda (u:
731 T).(\lambda (_: T).(ty3 g c0 w u))))))).(\lambda (t0: T).(\lambda (_: (ty3 g
732 c0 t2 t0)).(\lambda (_: (((eq T t2 (THead (Flat Appl) w v)) \to (ex3_2 T T
733 (\lambda (u: T).(\lambda (t: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind
734 Abst) u t)) t0))) (\lambda (u: T).(\lambda (t: T).(ty3 g c0 v (THead (Bind
735 Abst) u t)))) (\lambda (u: T).(\lambda (_: T).(ty3 g c0 w u))))))).(\lambda
736 (H5: (eq T (THead (Flat Cast) t2 t1) (THead (Flat Appl) w v))).(let H6 \def
737 (eq_ind T (THead (Flat Cast) t2 t1) (\lambda (ee: T).(match ee with [(TSort
738 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
739 \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow
740 (match f with [Appl \Rightarrow False | Cast \Rightarrow True])])])) I (THead
741 (Flat Appl) w v) H5) in (False_ind (ex3_2 T T (\lambda (u: T).(\lambda (t:
742 T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) (THead (Flat Cast)
743 t0 t2)))) (\lambda (u: T).(\lambda (t: T).(ty3 g c0 v (THead (Bind Abst) u
744 t)))) (\lambda (u: T).(\lambda (_: T).(ty3 g c0 w u)))) H6))))))))))) c y x
748 \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).(\forall
749 (x: T).((ty3 g c (THead (Flat Cast) t2 t1) x) \to (ex3 T (\lambda (t0:
750 T).(pc3 c (THead (Flat Cast) t0 t2) x)) (\lambda (_: T).(ty3 g c t1 t2))
751 (\lambda (t0: T).(ty3 g c t2 t0))))))))
753 \lambda (g: G).(\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
754 (x: T).(\lambda (H: (ty3 g c (THead (Flat Cast) t2 t1) x)).(insert_eq T
755 (THead (Flat Cast) t2 t1) (\lambda (t: T).(ty3 g c t x)) (\lambda (_: T).(ex3
756 T (\lambda (t0: T).(pc3 c (THead (Flat Cast) t0 t2) x)) (\lambda (_: T).(ty3
757 g c t1 t2)) (\lambda (t0: T).(ty3 g c t2 t0)))) (\lambda (y: T).(\lambda (H0:
758 (ty3 g c y x)).(ty3_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0:
759 T).((eq T t (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t3: T).(pc3 c0
760 (THead (Flat Cast) t3 t2) t0)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda
761 (t3: T).(ty3 g c0 t2 t3))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t:
762 T).(\lambda (_: (ty3 g c0 t0 t)).(\lambda (_: (((eq T t0 (THead (Flat Cast)
763 t2 t1)) \to (ex3 T (\lambda (t3: T).(pc3 c0 (THead (Flat Cast) t3 t2) t))
764 (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t3: T).(ty3 g c0 t2
765 t3)))))).(\lambda (u: T).(\lambda (t3: T).(\lambda (H3: (ty3 g c0 u
766 t3)).(\lambda (H4: (((eq T u (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda
767 (t4: T).(pc3 c0 (THead (Flat Cast) t4 t2) t3)) (\lambda (_: T).(ty3 g c0 t1
768 t2)) (\lambda (t4: T).(ty3 g c0 t2 t4)))))).(\lambda (H5: (pc3 c0 t3
769 t0)).(\lambda (H6: (eq T u (THead (Flat Cast) t2 t1))).(let H7 \def (f_equal
770 T T (\lambda (e: T).e) u (THead (Flat Cast) t2 t1) H6) in (let H8 \def
771 (eq_ind T u (\lambda (t4: T).((eq T t4 (THead (Flat Cast) t2 t1)) \to (ex3 T
772 (\lambda (t5: T).(pc3 c0 (THead (Flat Cast) t5 t2) t3)) (\lambda (_: T).(ty3
773 g c0 t1 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5))))) H4 (THead (Flat Cast) t2
774 t1) H7) in (let H9 \def (eq_ind T u (\lambda (t4: T).(ty3 g c0 t4 t3)) H3
775 (THead (Flat Cast) t2 t1) H7) in (let H10 \def (H8 (refl_equal T (THead (Flat
776 Cast) t2 t1))) in (ex3_ind T (\lambda (t4: T).(pc3 c0 (THead (Flat Cast) t4
777 t2) t3)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t4: T).(ty3 g c0 t2 t4))
778 (ex3 T (\lambda (t4: T).(pc3 c0 (THead (Flat Cast) t4 t2) t0)) (\lambda (_:
779 T).(ty3 g c0 t1 t2)) (\lambda (t4: T).(ty3 g c0 t2 t4))) (\lambda (x0:
780 T).(\lambda (H11: (pc3 c0 (THead (Flat Cast) x0 t2) t3)).(\lambda (H12: (ty3
781 g c0 t1 t2)).(\lambda (H13: (ty3 g c0 t2 x0)).(ex3_intro T (\lambda (t4:
782 T).(pc3 c0 (THead (Flat Cast) t4 t2) t0)) (\lambda (_: T).(ty3 g c0 t1 t2))
783 (\lambda (t4: T).(ty3 g c0 t2 t4)) x0 (pc3_t t3 c0 (THead (Flat Cast) x0 t2)
784 H11 t0 H5) H12 H13))))) H10)))))))))))))))) (\lambda (c0: C).(\lambda (m:
785 nat).(\lambda (H1: (eq T (TSort m) (THead (Flat Cast) t2 t1))).(let H2 \def
786 (eq_ind T (TSort m) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow
787 True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I
788 (THead (Flat Cast) t2 t1) H1) in (False_ind (ex3 T (\lambda (t0: T).(pc3 c0
789 (THead (Flat Cast) t0 t2) (TSort (next g m)))) (\lambda (_: T).(ty3 g c0 t1
790 t2)) (\lambda (t0: T).(ty3 g c0 t2 t0))) H2))))) (\lambda (n: nat).(\lambda
791 (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (_: (getl n c0 (CHead d
792 (Bind Abbr) u))).(\lambda (t: T).(\lambda (_: (ty3 g d u t)).(\lambda (_:
793 (((eq T u (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t0: T).(pc3 d
794 (THead (Flat Cast) t0 t2) t)) (\lambda (_: T).(ty3 g d t1 t2)) (\lambda (t0:
795 T).(ty3 g d t2 t0)))))).(\lambda (H4: (eq T (TLRef n) (THead (Flat Cast) t2
796 t1))).(let H5 \def (eq_ind T (TLRef n) (\lambda (ee: T).(match ee with
797 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _)
798 \Rightarrow False])) I (THead (Flat Cast) t2 t1) H4) in (False_ind (ex3 T
799 (\lambda (t0: T).(pc3 c0 (THead (Flat Cast) t0 t2) (lift (S n) O t)))
800 (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t0: T).(ty3 g c0 t2 t0)))
801 H5))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u:
802 T).(\lambda (_: (getl n c0 (CHead d (Bind Abst) u))).(\lambda (t: T).(\lambda
803 (_: (ty3 g d u t)).(\lambda (_: (((eq T u (THead (Flat Cast) t2 t1)) \to (ex3
804 T (\lambda (t0: T).(pc3 d (THead (Flat Cast) t0 t2) t)) (\lambda (_: T).(ty3
805 g d t1 t2)) (\lambda (t0: T).(ty3 g d t2 t0)))))).(\lambda (H4: (eq T (TLRef
806 n) (THead (Flat Cast) t2 t1))).(let H5 \def (eq_ind T (TLRef n) (\lambda (ee:
807 T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
808 (THead _ _ _) \Rightarrow False])) I (THead (Flat Cast) t2 t1) H4) in
809 (False_ind (ex3 T (\lambda (t0: T).(pc3 c0 (THead (Flat Cast) t0 t2) (lift (S
810 n) O u))) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t0: T).(ty3 g c0 t2
811 t0))) H5))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda (t: T).(\lambda
812 (_: (ty3 g c0 u t)).(\lambda (_: (((eq T u (THead (Flat Cast) t2 t1)) \to
813 (ex3 T (\lambda (t0: T).(pc3 c0 (THead (Flat Cast) t0 t2) t)) (\lambda (_:
814 T).(ty3 g c0 t1 t2)) (\lambda (t0: T).(ty3 g c0 t2 t0)))))).(\lambda (b:
815 B).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3 g (CHead c0 (Bind b)
816 u) t0 t3)).(\lambda (_: (((eq T t0 (THead (Flat Cast) t2 t1)) \to (ex3 T
817 (\lambda (t4: T).(pc3 (CHead c0 (Bind b) u) (THead (Flat Cast) t4 t2) t3))
818 (\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t2)) (\lambda (t4: T).(ty3 g
819 (CHead c0 (Bind b) u) t2 t4)))))).(\lambda (H5: (eq T (THead (Bind b) u t0)
820 (THead (Flat Cast) t2 t1))).(let H6 \def (eq_ind T (THead (Bind b) u t0)
821 (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
822 \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _)
823 \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat Cast) t2
824 t1) H5) in (False_ind (ex3 T (\lambda (t4: T).(pc3 c0 (THead (Flat Cast) t4
825 t2) (THead (Bind b) u t3))) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t4:
826 T).(ty3 g c0 t2 t4))) H6))))))))))))) (\lambda (c0: C).(\lambda (w:
827 T).(\lambda (u: T).(\lambda (_: (ty3 g c0 w u)).(\lambda (_: (((eq T w (THead
828 (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t0: T).(pc3 c0 (THead (Flat Cast) t0
829 t2) u)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t0: T).(ty3 g c0 t2
830 t0)))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 v (THead
831 (Bind Abst) u t))).(\lambda (_: (((eq T v (THead (Flat Cast) t2 t1)) \to (ex3
832 T (\lambda (t0: T).(pc3 c0 (THead (Flat Cast) t0 t2) (THead (Bind Abst) u
833 t))) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t0: T).(ty3 g c0 t2
834 t0)))))).(\lambda (H5: (eq T (THead (Flat Appl) w v) (THead (Flat Cast) t2
835 t1))).(let H6 \def (eq_ind T (THead (Flat Appl) w v) (\lambda (ee: T).(match
836 ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k
837 _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat f)
838 \Rightarrow (match f with [Appl \Rightarrow True | Cast \Rightarrow
839 False])])])) I (THead (Flat Cast) t2 t1) H5) in (False_ind (ex3 T (\lambda
840 (t0: T).(pc3 c0 (THead (Flat Cast) t0 t2) (THead (Flat Appl) w (THead (Bind
841 Abst) u t)))) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t0: T).(ty3 g c0 t2
842 t0))) H6)))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t3:
843 T).(\lambda (H1: (ty3 g c0 t0 t3)).(\lambda (H2: (((eq T t0 (THead (Flat
844 Cast) t2 t1)) \to (ex3 T (\lambda (t4: T).(pc3 c0 (THead (Flat Cast) t4 t2)
845 t3)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t4: T).(ty3 g c0 t2
846 t4)))))).(\lambda (t4: T).(\lambda (H3: (ty3 g c0 t3 t4)).(\lambda (H4: (((eq
847 T t3 (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t5: T).(pc3 c0 (THead
848 (Flat Cast) t5 t2) t4)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t5:
849 T).(ty3 g c0 t2 t5)))))).(\lambda (H5: (eq T (THead (Flat Cast) t3 t0) (THead
850 (Flat Cast) t2 t1))).(let H6 \def (f_equal T T (\lambda (e: T).(match e with
851 [(TSort _) \Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ t _)
852 \Rightarrow t])) (THead (Flat Cast) t3 t0) (THead (Flat Cast) t2 t1) H5) in
853 ((let H7 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
854 \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) \Rightarrow t]))
855 (THead (Flat Cast) t3 t0) (THead (Flat Cast) t2 t1) H5) in (\lambda (H8: (eq
856 T t3 t2)).(let H9 \def (eq_ind T t3 (\lambda (t: T).((eq T t (THead (Flat
857 Cast) t2 t1)) \to (ex3 T (\lambda (t5: T).(pc3 c0 (THead (Flat Cast) t5 t2)
858 t4)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5)))))
859 H4 t2 H8) in (let H10 \def (eq_ind T t3 (\lambda (t: T).(ty3 g c0 t t4)) H3
860 t2 H8) in (let H11 \def (eq_ind T t3 (\lambda (t: T).((eq T t0 (THead (Flat
861 Cast) t2 t1)) \to (ex3 T (\lambda (t5: T).(pc3 c0 (THead (Flat Cast) t5 t2)
862 t)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5)))))
863 H2 t2 H8) in (let H12 \def (eq_ind T t3 (\lambda (t: T).(ty3 g c0 t0 t)) H1
864 t2 H8) in (eq_ind_r T t2 (\lambda (t: T).(ex3 T (\lambda (t5: T).(pc3 c0
865 (THead (Flat Cast) t5 t2) (THead (Flat Cast) t4 t))) (\lambda (_: T).(ty3 g
866 c0 t1 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5)))) (let H13 \def (eq_ind T t0
867 (\lambda (t: T).((eq T t (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t5:
868 T).(pc3 c0 (THead (Flat Cast) t5 t2) t2)) (\lambda (_: T).(ty3 g c0 t1 t2))
869 (\lambda (t5: T).(ty3 g c0 t2 t5))))) H11 t1 H7) in (let H14 \def (eq_ind T
870 t0 (\lambda (t: T).(ty3 g c0 t t2)) H12 t1 H7) in (ex3_intro T (\lambda (t5:
871 T).(pc3 c0 (THead (Flat Cast) t5 t2) (THead (Flat Cast) t4 t2))) (\lambda (_:
872 T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5)) t4 (pc3_refl c0
873 (THead (Flat Cast) t4 t2)) H14 H10))) t3 H8))))))) H6))))))))))) c y x H0)))
877 \forall (g: G).(\forall (c: C).(\forall (u: T).((tys3 g c TNil u) \to (ex T
878 (\lambda (u0: T).(ty3 g c u u0))))))
880 \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (H: (tys3 g c TNil
881 u)).(insert_eq TList TNil (\lambda (t: TList).(tys3 g c t u)) (\lambda (_:
882 TList).(ex T (\lambda (u0: T).(ty3 g c u u0)))) (\lambda (y: TList).(\lambda
883 (H0: (tys3 g c y u)).(tys3_ind g c (\lambda (t: TList).(\lambda (t0: T).((eq
884 TList t TNil) \to (ex T (\lambda (u0: T).(ty3 g c t0 u0)))))) (\lambda (u0:
885 T).(\lambda (u1: T).(\lambda (H1: (ty3 g c u0 u1)).(\lambda (_: (eq TList
886 TNil TNil)).(ex_intro T (\lambda (u2: T).(ty3 g c u0 u2)) u1 H1))))) (\lambda
887 (t: T).(\lambda (u0: T).(\lambda (_: (ty3 g c t u0)).(\lambda (ts:
888 TList).(\lambda (_: (tys3 g c ts u0)).(\lambda (_: (((eq TList ts TNil) \to
889 (ex T (\lambda (u1: T).(ty3 g c u0 u1)))))).(\lambda (H4: (eq TList (TCons t
890 ts) TNil)).(let H5 \def (eq_ind TList (TCons t ts) (\lambda (ee:
891 TList).(match ee with [TNil \Rightarrow False | (TCons _ _) \Rightarrow
892 True])) I TNil H4) in (False_ind (ex T (\lambda (u1: T).(ty3 g c u0 u1)))
893 H5))))))))) y u H0))) H)))).
896 \forall (g: G).(\forall (c: C).(\forall (ts: TList).(\forall (t: T).(\forall
897 (u: T).((tys3 g c (TCons t ts) u) \to (land (ty3 g c t u) (tys3 g c ts
900 \lambda (g: G).(\lambda (c: C).(\lambda (ts: TList).(\lambda (t: T).(\lambda
901 (u: T).(\lambda (H: (tys3 g c (TCons t ts) u)).(insert_eq TList (TCons t ts)
902 (\lambda (t0: TList).(tys3 g c t0 u)) (\lambda (_: TList).(land (ty3 g c t u)
903 (tys3 g c ts u))) (\lambda (y: TList).(\lambda (H0: (tys3 g c y u)).(tys3_ind
904 g c (\lambda (t0: TList).(\lambda (t1: T).((eq TList t0 (TCons t ts)) \to
905 (land (ty3 g c t t1) (tys3 g c ts t1))))) (\lambda (u0: T).(\lambda (u1:
906 T).(\lambda (_: (ty3 g c u0 u1)).(\lambda (H2: (eq TList TNil (TCons t
907 ts))).(let H3 \def (eq_ind TList TNil (\lambda (ee: TList).(match ee with
908 [TNil \Rightarrow True | (TCons _ _) \Rightarrow False])) I (TCons t ts) H2)
909 in (False_ind (land (ty3 g c t u0) (tys3 g c ts u0)) H3)))))) (\lambda (t0:
910 T).(\lambda (u0: T).(\lambda (H1: (ty3 g c t0 u0)).(\lambda (ts0:
911 TList).(\lambda (H2: (tys3 g c ts0 u0)).(\lambda (H3: (((eq TList ts0 (TCons
912 t ts)) \to (land (ty3 g c t u0) (tys3 g c ts u0))))).(\lambda (H4: (eq TList
913 (TCons t0 ts0) (TCons t ts))).(let H5 \def (f_equal TList T (\lambda (e:
914 TList).(match e with [TNil \Rightarrow t0 | (TCons t1 _) \Rightarrow t1]))
915 (TCons t0 ts0) (TCons t ts) H4) in ((let H6 \def (f_equal TList TList
916 (\lambda (e: TList).(match e with [TNil \Rightarrow ts0 | (TCons _ t1)
917 \Rightarrow t1])) (TCons t0 ts0) (TCons t ts) H4) in (\lambda (H7: (eq T t0
918 t)).(let H8 \def (eq_ind TList ts0 (\lambda (t1: TList).((eq TList t1 (TCons
919 t ts)) \to (land (ty3 g c t u0) (tys3 g c ts u0)))) H3 ts H6) in (let H9 \def
920 (eq_ind TList ts0 (\lambda (t1: TList).(tys3 g c t1 u0)) H2 ts H6) in (let
921 H10 \def (eq_ind T t0 (\lambda (t1: T).(ty3 g c t1 u0)) H1 t H7) in (conj
922 (ty3 g c t u0) (tys3 g c ts u0) H10 H9)))))) H5))))))))) y u H0))) H)))))).
projects / helm.git / blob