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/sty0/defs.ma".
19 theorem sty0_gen_sort:
20 \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((sty0 g c
21 (TSort n) x) \to (eq T x (TSort (next g n)))))))
23 \lambda (g: G).(\lambda (c: C).(\lambda (x: T).(\lambda (n: nat).(\lambda
24 (H: (sty0 g c (TSort n) x)).(insert_eq T (TSort n) (\lambda (t: T).(sty0 g c
25 t x)) (\lambda (_: T).(eq T x (TSort (next g n)))) (\lambda (y: T).(\lambda
26 (H0: (sty0 g c y x)).(sty0_ind g (\lambda (_: C).(\lambda (t: T).(\lambda
27 (t0: T).((eq T t (TSort n)) \to (eq T t0 (TSort (next g n))))))) (\lambda (_:
28 C).(\lambda (n0: nat).(\lambda (H1: (eq T (TSort n0) (TSort n))).(let H2 \def
29 (f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with
30 [(TSort n1) \Rightarrow n1 | (TLRef _) \Rightarrow n0 | (THead _ _ _)
31 \Rightarrow n0])) (TSort n0) (TSort n) H1) in (eq_ind_r nat n (\lambda (n1:
32 nat).(eq T (TSort (next g n1)) (TSort (next g n)))) (refl_equal T (TSort
33 (next g n))) n0 H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (v:
34 T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind Abbr)
35 v))).(\lambda (w: T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T v
36 (TSort n)) \to (eq T w (TSort (next g n)))))).(\lambda (H4: (eq T (TLRef i)
37 (TSort n))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T
38 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
39 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n) H4) in
40 (False_ind (eq T (lift (S i) O w) (TSort (next g n))) H5))))))))))) (\lambda
41 (c0: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl
42 i c0 (CHead d (Bind Abst) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v
43 w)).(\lambda (_: (((eq T v (TSort n)) \to (eq T w (TSort (next g
44 n)))))).(\lambda (H4: (eq T (TLRef i) (TSort n))).(let H5 \def (eq_ind T
45 (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with
46 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _)
47 \Rightarrow False])) I (TSort n) H4) in (False_ind (eq T (lift (S i) O v)
48 (TSort (next g n))) H5))))))))))) (\lambda (b: B).(\lambda (c0: C).(\lambda
49 (v: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (sty0 g (CHead c0 (Bind
50 b) v) t1 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq T t2 (TSort (next g
51 n)))))).(\lambda (H3: (eq T (THead (Bind b) v t1) (TSort n))).(let H4 \def
52 (eq_ind T (THead (Bind b) v t1) (\lambda (ee: T).(match ee in T return
53 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
54 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H3) in
55 (False_ind (eq T (THead (Bind b) v t2) (TSort (next g n))) H4))))))))))
56 (\lambda (c0: C).(\lambda (v: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda
57 (_: (sty0 g c0 t1 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq T t2 (TSort
58 (next g n)))))).(\lambda (H3: (eq T (THead (Flat Appl) v t1) (TSort n))).(let
59 H4 \def (eq_ind T (THead (Flat Appl) v t1) (\lambda (ee: T).(match ee in T
60 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
61 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H3) in
62 (False_ind (eq T (THead (Flat Appl) v t2) (TSort (next g n))) H4)))))))))
63 (\lambda (c0: C).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (sty0 g c0 v1
64 v2)).(\lambda (_: (((eq T v1 (TSort n)) \to (eq T v2 (TSort (next g
65 n)))))).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (sty0 g c0 t1
66 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq T t2 (TSort (next g
67 n)))))).(\lambda (H5: (eq T (THead (Flat Cast) v1 t1) (TSort n))).(let H6
68 \def (eq_ind T (THead (Flat Cast) v1 t1) (\lambda (ee: T).(match ee in T
69 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
70 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H5) in
71 (False_ind (eq T (THead (Flat Cast) v2 t2) (TSort (next g n))) H6))))))))))))
77 theorem sty0_gen_lref:
78 \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((sty0 g c
79 (TLRef n) x) \to (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda
80 (_: T).(getl n c (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
81 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda
82 (t: T).(eq T x (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda
83 (u: T).(\lambda (_: T).(getl n c (CHead e (Bind Abst) u))))) (\lambda (e:
84 C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda
85 (u: T).(\lambda (_: T).(eq T x (lift (S n) O u)))))))))))
87 \lambda (g: G).(\lambda (c: C).(\lambda (x: T).(\lambda (n: nat).(\lambda
88 (H: (sty0 g c (TLRef n) x)).(insert_eq T (TLRef n) (\lambda (t: T).(sty0 g c
89 t x)) (\lambda (_: T).(or (ex3_3 C T T (\lambda (e: C).(\lambda (u:
90 T).(\lambda (_: T).(getl n c (CHead e (Bind Abbr) u))))) (\lambda (e:
91 C).(\lambda (u: T).(\lambda (t0: T).(sty0 g e u t0)))) (\lambda (_:
92 C).(\lambda (_: T).(\lambda (t0: T).(eq T x (lift (S n) O t0)))))) (ex3_3 C T
93 T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c (CHead e (Bind
94 Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t0: T).(sty0 g e u
95 t0)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T x (lift (S n) O
96 u)))))))) (\lambda (y: T).(\lambda (H0: (sty0 g c y x)).(sty0_ind g (\lambda
97 (c0: C).(\lambda (t: T).(\lambda (t0: T).((eq T t (TLRef n)) \to (or (ex3_3 C
98 T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
99 Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t1: T).(sty0 g e u
100 t1)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t1: T).(eq T t0 (lift (S n)
101 O t1)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl
102 n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda
103 (t1: T).(sty0 g e u t1)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_:
104 T).(eq T t0 (lift (S n) O u))))))))))) (\lambda (c0: C).(\lambda (n0:
105 nat).(\lambda (H1: (eq T (TSort n0) (TLRef n))).(let H2 \def (eq_ind T (TSort
106 n0) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
107 _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
108 False])) I (TLRef n) H1) in (False_ind (or (ex3_3 C T T (\lambda (e:
109 C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u)))))
110 (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda
111 (_: C).(\lambda (_: T).(\lambda (t: T).(eq T (TSort (next g n0)) (lift (S n)
112 O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl
113 n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t:
114 T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T
115 (TSort (next g n0)) (lift (S n) O u))))))) H2))))) (\lambda (c0: C).(\lambda
116 (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H1: (getl i c0 (CHead d
117 (Bind Abbr) v))).(\lambda (w: T).(\lambda (H2: (sty0 g d v w)).(\lambda (_:
118 (((eq T v (TLRef n)) \to (or (ex3_3 C T T (\lambda (e: C).(\lambda (u:
119 T).(\lambda (_: T).(getl n d (CHead e (Bind Abbr) u))))) (\lambda (e:
120 C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda
121 (_: T).(\lambda (t: T).(eq T w (lift (S n) O t)))))) (ex3_3 C T T (\lambda
122 (e: C).(\lambda (u: T).(\lambda (_: T).(getl n d (CHead e (Bind Abst) u)))))
123 (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda
124 (_: C).(\lambda (u: T).(\lambda (_: T).(eq T w (lift (S n) O
125 u)))))))))).(\lambda (H4: (eq T (TLRef i) (TLRef n))).(let H5 \def (f_equal T
126 nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _)
127 \Rightarrow i | (TLRef n0) \Rightarrow n0 | (THead _ _ _) \Rightarrow i]))
128 (TLRef i) (TLRef n) H4) in (let H6 \def (eq_ind nat i (\lambda (n0:
129 nat).(getl n0 c0 (CHead d (Bind Abbr) v))) H1 n H5) in (eq_ind_r nat n
130 (\lambda (n0: nat).(or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda
131 (_: T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
132 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda
133 (t: T).(eq T (lift (S n0) O w) (lift (S n) O t)))))) (ex3_3 C T T (\lambda
134 (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u)))))
135 (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda
136 (_: C).(\lambda (u: T).(\lambda (_: T).(eq T (lift (S n0) O w) (lift (S n) O
137 u)))))))) (or_introl (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda
138 (_: T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
139 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda
140 (t: T).(eq T (lift (S n) O w) (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e:
141 C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u)))))
142 (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda
143 (_: C).(\lambda (u: T).(\lambda (_: T).(eq T (lift (S n) O w) (lift (S n) O
144 u)))))) (ex3_3_intro C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_:
145 T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
146 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda
147 (t: T).(eq T (lift (S n) O w) (lift (S n) O t))))) d v w H6 H2 (refl_equal T
148 (lift (S n) O w)))) i H5)))))))))))) (\lambda (c0: C).(\lambda (d:
149 C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H1: (getl i c0 (CHead d (Bind
150 Abst) v))).(\lambda (w: T).(\lambda (H2: (sty0 g d v w)).(\lambda (_: (((eq T
151 v (TLRef n)) \to (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda
152 (_: T).(getl n d (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
153 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda
154 (t: T).(eq T w (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda
155 (u: T).(\lambda (_: T).(getl n d (CHead e (Bind Abst) u))))) (\lambda (e:
156 C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda
157 (u: T).(\lambda (_: T).(eq T w (lift (S n) O u)))))))))).(\lambda (H4: (eq T
158 (TLRef i) (TLRef n))).(let H5 \def (f_equal T nat (\lambda (e: T).(match e in
159 T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow i | (TLRef n0)
160 \Rightarrow n0 | (THead _ _ _) \Rightarrow i])) (TLRef i) (TLRef n) H4) in
161 (let H6 \def (eq_ind nat i (\lambda (n0: nat).(getl n0 c0 (CHead d (Bind
162 Abst) v))) H1 n H5) in (eq_ind_r nat n (\lambda (n0: nat).(or (ex3_3 C T T
163 (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
164 Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u
165 t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T (lift (S n0) O v)
166 (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda
167 (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u:
168 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda
169 (_: T).(eq T (lift (S n0) O v) (lift (S n) O u)))))))) (or_intror (ex3_3 C T
170 T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
171 Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u
172 t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T (lift (S n) O v)
173 (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda
174 (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u:
175 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda
176 (_: T).(eq T (lift (S n) O v) (lift (S n) O u)))))) (ex3_3_intro C T T
177 (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
178 Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u
179 t)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T (lift (S n) O v)
180 (lift (S n) O u))))) d v w H6 H2 (refl_equal T (lift (S n) O v)))) i
181 H5)))))))))))) (\lambda (b: B).(\lambda (c0: C).(\lambda (v: T).(\lambda (t1:
182 T).(\lambda (t2: T).(\lambda (_: (sty0 g (CHead c0 (Bind b) v) t1
183 t2)).(\lambda (_: (((eq T t1 (TLRef n)) \to (or (ex3_3 C T T (\lambda (e:
184 C).(\lambda (u: T).(\lambda (_: T).(getl n (CHead c0 (Bind b) v) (CHead e
185 (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e
186 u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T t2 (lift (S n)
187 O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl
188 n (CHead c0 (Bind b) v) (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda
189 (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u:
190 T).(\lambda (_: T).(eq T t2 (lift (S n) O u)))))))))).(\lambda (H3: (eq T
191 (THead (Bind b) v t1) (TLRef n))).(let H4 \def (eq_ind T (THead (Bind b) v
192 t1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
193 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
194 \Rightarrow True])) I (TLRef n) H3) in (False_ind (or (ex3_3 C T T (\lambda
195 (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u)))))
196 (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda
197 (_: C).(\lambda (_: T).(\lambda (t: T).(eq T (THead (Bind b) v t2) (lift (S
198 n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_:
199 T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u:
200 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda
201 (_: T).(eq T (THead (Bind b) v t2) (lift (S n) O u))))))) H4))))))))))
202 (\lambda (c0: C).(\lambda (v: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda
203 (_: (sty0 g c0 t1 t2)).(\lambda (_: (((eq T t1 (TLRef n)) \to (or (ex3_3 C T
204 T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
205 Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u
206 t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T t2 (lift (S n) O
207 t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n
208 c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t:
209 T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T t2
210 (lift (S n) O u)))))))))).(\lambda (H3: (eq T (THead (Flat Appl) v t1) (TLRef
211 n))).(let H4 \def (eq_ind T (THead (Flat Appl) v t1) (\lambda (ee: T).(match
212 ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False |
213 (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n)
214 H3) in (False_ind (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda
215 (_: T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
216 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda
217 (t: T).(eq T (THead (Flat Appl) v t2) (lift (S n) O t)))))) (ex3_3 C T T
218 (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
219 Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u
220 t)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T (THead (Flat
221 Appl) v t2) (lift (S n) O u))))))) H4))))))))) (\lambda (c0: C).(\lambda (v1:
222 T).(\lambda (v2: T).(\lambda (_: (sty0 g c0 v1 v2)).(\lambda (_: (((eq T v1
223 (TLRef n)) \to (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_:
224 T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
225 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda
226 (t: T).(eq T v2 (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda
227 (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e:
228 C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda
229 (u: T).(\lambda (_: T).(eq T v2 (lift (S n) O u)))))))))).(\lambda (t1:
230 T).(\lambda (t2: T).(\lambda (_: (sty0 g c0 t1 t2)).(\lambda (_: (((eq T t1
231 (TLRef n)) \to (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_:
232 T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
233 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda
234 (t: T).(eq T t2 (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda
235 (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e:
236 C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda
237 (u: T).(\lambda (_: T).(eq T t2 (lift (S n) O u)))))))))).(\lambda (H5: (eq T
238 (THead (Flat Cast) v1 t1) (TLRef n))).(let H6 \def (eq_ind T (THead (Flat
239 Cast) v1 t1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop)
240 with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _
241 _) \Rightarrow True])) I (TLRef n) H5) in (False_ind (or (ex3_3 C T T
242 (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
243 Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u
244 t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T (THead (Flat
245 Cast) v2 t2) (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u:
246 T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e:
247 C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda
248 (u: T).(\lambda (_: T).(eq T (THead (Flat Cast) v2 t2) (lift (S n) O u)))))))
249 H6)))))))))))) c y x H0))) H))))).
254 theorem sty0_gen_bind:
255 \forall (g: G).(\forall (b: B).(\forall (c: C).(\forall (u: T).(\forall (t1:
256 T).(\forall (x: T).((sty0 g c (THead (Bind b) u t1) x) \to (ex2 T (\lambda
257 (t2: T).(sty0 g (CHead c (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T x (THead
258 (Bind b) u t2))))))))))
260 \lambda (g: G).(\lambda (b: B).(\lambda (c: C).(\lambda (u: T).(\lambda (t1:
261 T).(\lambda (x: T).(\lambda (H: (sty0 g c (THead (Bind b) u t1)
262 x)).(insert_eq T (THead (Bind b) u t1) (\lambda (t: T).(sty0 g c t x))
263 (\lambda (_: T).(ex2 T (\lambda (t2: T).(sty0 g (CHead c (Bind b) u) t1 t2))
264 (\lambda (t2: T).(eq T x (THead (Bind b) u t2))))) (\lambda (y: T).(\lambda
265 (H0: (sty0 g c y x)).(sty0_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda
266 (t0: T).((eq T t (THead (Bind b) u t1)) \to (ex2 T (\lambda (t2: T).(sty0 g
267 (CHead c0 (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T t0 (THead (Bind b) u
268 t2)))))))) (\lambda (c0: C).(\lambda (n: nat).(\lambda (H1: (eq T (TSort n)
269 (THead (Bind b) u t1))).(let H2 \def (eq_ind T (TSort n) (\lambda (ee:
270 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
271 True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I
272 (THead (Bind b) u t1) H1) in (False_ind (ex2 T (\lambda (t2: T).(sty0 g
273 (CHead c0 (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T (TSort (next g n))
274 (THead (Bind b) u t2)))) H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda
275 (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind Abbr)
276 v))).(\lambda (w: T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T v
277 (THead (Bind b) u t1)) \to (ex2 T (\lambda (t2: T).(sty0 g (CHead d (Bind b)
278 u) t1 t2)) (\lambda (t2: T).(eq T w (THead (Bind b) u t2))))))).(\lambda (H4:
279 (eq T (TLRef i) (THead (Bind b) u t1))).(let H5 \def (eq_ind T (TLRef i)
280 (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
281 \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow
282 False])) I (THead (Bind b) u t1) H4) in (False_ind (ex2 T (\lambda (t2:
283 T).(sty0 g (CHead c0 (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T (lift (S i) O
284 w) (THead (Bind b) u t2)))) H5))))))))))) (\lambda (c0: C).(\lambda (d:
285 C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind
286 Abst) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T
287 v (THead (Bind b) u t1)) \to (ex2 T (\lambda (t2: T).(sty0 g (CHead d (Bind
288 b) u) t1 t2)) (\lambda (t2: T).(eq T w (THead (Bind b) u t2))))))).(\lambda
289 (H4: (eq T (TLRef i) (THead (Bind b) u t1))).(let H5 \def (eq_ind T (TLRef i)
290 (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
291 \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow
292 False])) I (THead (Bind b) u t1) H4) in (False_ind (ex2 T (\lambda (t2:
293 T).(sty0 g (CHead c0 (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T (lift (S i) O
294 v) (THead (Bind b) u t2)))) H5))))))))))) (\lambda (b0: B).(\lambda (c0:
295 C).(\lambda (v: T).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H1: (sty0 g
296 (CHead c0 (Bind b0) v) t0 t2)).(\lambda (H2: (((eq T t0 (THead (Bind b) u
297 t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead (CHead c0 (Bind b0) v) (Bind
298 b) u) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3))))))).(\lambda
299 (H3: (eq T (THead (Bind b0) v t0) (THead (Bind b) u t1))).(let H4 \def
300 (f_equal T B (\lambda (e: T).(match e in T return (\lambda (_: T).B) with
301 [(TSort _) \Rightarrow b0 | (TLRef _) \Rightarrow b0 | (THead k _ _)
302 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b1)
303 \Rightarrow b1 | (Flat _) \Rightarrow b0])])) (THead (Bind b0) v t0) (THead
304 (Bind b) u t1) H3) in ((let H5 \def (f_equal T T (\lambda (e: T).(match e in
305 T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v | (TLRef _)
306 \Rightarrow v | (THead _ t _) \Rightarrow t])) (THead (Bind b0) v t0) (THead
307 (Bind b) u t1) H3) in ((let H6 \def (f_equal T T (\lambda (e: T).(match e in
308 T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _)
309 \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead (Bind b0) v t0) (THead
310 (Bind b) u t1) H3) in (\lambda (H7: (eq T v u)).(\lambda (H8: (eq B b0
311 b)).(let H9 \def (eq_ind T t0 (\lambda (t: T).((eq T t (THead (Bind b) u t1))
312 \to (ex2 T (\lambda (t3: T).(sty0 g (CHead (CHead c0 (Bind b0) v) (Bind b) u)
313 t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3)))))) H2 t1 H6) in
314 (let H10 \def (eq_ind T t0 (\lambda (t: T).(sty0 g (CHead c0 (Bind b0) v) t
315 t2)) H1 t1 H6) in (let H11 \def (eq_ind T v (\lambda (t: T).((eq T t1 (THead
316 (Bind b) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead (CHead c0 (Bind
317 b0) t) (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u
318 t3)))))) H9 u H7) in (let H12 \def (eq_ind T v (\lambda (t: T).(sty0 g (CHead
319 c0 (Bind b0) t) t1 t2)) H10 u H7) in (eq_ind_r T u (\lambda (t: T).(ex2 T
320 (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T
321 (THead (Bind b0) t t2) (THead (Bind b) u t3))))) (let H13 \def (eq_ind B b0
322 (\lambda (b1: B).((eq T t1 (THead (Bind b) u t1)) \to (ex2 T (\lambda (t3:
323 T).(sty0 g (CHead (CHead c0 (Bind b1) u) (Bind b) u) t1 t3)) (\lambda (t3:
324 T).(eq T t2 (THead (Bind b) u t3)))))) H11 b H8) in (let H14 \def (eq_ind B
325 b0 (\lambda (b1: B).(sty0 g (CHead c0 (Bind b1) u) t1 t2)) H12 b H8) in
326 (eq_ind_r B b (\lambda (b1: B).(ex2 T (\lambda (t3: T).(sty0 g (CHead c0
327 (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T (THead (Bind b1) u t2) (THead
328 (Bind b) u t3))))) (ex_intro2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b)
329 u) t1 t3)) (\lambda (t3: T).(eq T (THead (Bind b) u t2) (THead (Bind b) u
330 t3))) t2 H14 (refl_equal T (THead (Bind b) u t2))) b0 H8))) v H7)))))))) H5))
331 H4)))))))))) (\lambda (c0: C).(\lambda (v: T).(\lambda (t0: T).(\lambda (t2:
332 T).(\lambda (_: (sty0 g c0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind b) u
333 t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) u) t1 t3))
334 (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3))))))).(\lambda (H3: (eq T
335 (THead (Flat Appl) v t0) (THead (Bind b) u t1))).(let H4 \def (eq_ind T
336 (THead (Flat Appl) v t0) (\lambda (ee: T).(match ee in T return (\lambda (_:
337 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
338 (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with
339 [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind
340 b) u t1) H3) in (False_ind (ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b)
341 u) t1 t3)) (\lambda (t3: T).(eq T (THead (Flat Appl) v t2) (THead (Bind b) u
342 t3)))) H4))))))))) (\lambda (c0: C).(\lambda (v1: T).(\lambda (v2:
343 T).(\lambda (_: (sty0 g c0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind b) u
344 t1)) \to (ex2 T (\lambda (t2: T).(sty0 g (CHead c0 (Bind b) u) t1 t2))
345 (\lambda (t2: T).(eq T v2 (THead (Bind b) u t2))))))).(\lambda (t0:
346 T).(\lambda (t2: T).(\lambda (_: (sty0 g c0 t0 t2)).(\lambda (_: (((eq T t0
347 (THead (Bind b) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b)
348 u) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3))))))).(\lambda
349 (H5: (eq T (THead (Flat Cast) v1 t0) (THead (Bind b) u t1))).(let H6 \def
350 (eq_ind T (THead (Flat Cast) v1 t0) (\lambda (ee: T).(match ee in T return
351 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
352 \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda
353 (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
354 True])])) I (THead (Bind b) u t1) H5) in (False_ind (ex2 T (\lambda (t3:
355 T).(sty0 g (CHead c0 (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T (THead (Flat
356 Cast) v2 t2) (THead (Bind b) u t3)))) H6)))))))))))) c y x H0))) H))))))).
361 theorem sty0_gen_appl:
362 \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall (x:
363 T).((sty0 g c (THead (Flat Appl) u t1) x) \to (ex2 T (\lambda (t2: T).(sty0 g
364 c t1 t2)) (\lambda (t2: T).(eq T x (THead (Flat Appl) u t2)))))))))
366 \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t1: T).(\lambda (x:
367 T).(\lambda (H: (sty0 g c (THead (Flat Appl) u t1) x)).(insert_eq T (THead
368 (Flat Appl) u t1) (\lambda (t: T).(sty0 g c t x)) (\lambda (_: T).(ex2 T
369 (\lambda (t2: T).(sty0 g c t1 t2)) (\lambda (t2: T).(eq T x (THead (Flat
370 Appl) u t2))))) (\lambda (y: T).(\lambda (H0: (sty0 g c y x)).(sty0_ind g
371 (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).((eq T t (THead (Flat Appl)
372 u t1)) \to (ex2 T (\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T
373 t0 (THead (Flat Appl) u t2)))))))) (\lambda (c0: C).(\lambda (n:
374 nat).(\lambda (H1: (eq T (TSort n) (THead (Flat Appl) u t1))).(let H2 \def
375 (eq_ind T (TSort n) (\lambda (ee: T).(match ee in T return (\lambda (_:
376 T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
377 (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) u t1) H1) in
378 (False_ind (ex2 T (\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T
379 (TSort (next g n)) (THead (Flat Appl) u t2)))) H2))))) (\lambda (c0:
380 C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0
381 (CHead d (Bind Abbr) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v
382 w)).(\lambda (_: (((eq T v (THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t2:
383 T).(sty0 g d t1 t2)) (\lambda (t2: T).(eq T w (THead (Flat Appl) u
384 t2))))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat Appl) u t1))).(let H5
385 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_:
386 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
387 (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) u t1) H4) in
388 (False_ind (ex2 T (\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T
389 (lift (S i) O w) (THead (Flat Appl) u t2)))) H5))))))))))) (\lambda (c0:
390 C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0
391 (CHead d (Bind Abst) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v
392 w)).(\lambda (_: (((eq T v (THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t2:
393 T).(sty0 g d t1 t2)) (\lambda (t2: T).(eq T w (THead (Flat Appl) u
394 t2))))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat Appl) u t1))).(let H5
395 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_:
396 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
397 (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) u t1) H4) in
398 (False_ind (ex2 T (\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T
399 (lift (S i) O v) (THead (Flat Appl) u t2)))) H5))))))))))) (\lambda (b:
400 B).(\lambda (c0: C).(\lambda (v: T).(\lambda (t0: T).(\lambda (t2:
401 T).(\lambda (_: (sty0 g (CHead c0 (Bind b) v) t0 t2)).(\lambda (_: (((eq T t0
402 (THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind
403 b) v) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Flat Appl) u
404 t3))))))).(\lambda (H3: (eq T (THead (Bind b) v t0) (THead (Flat Appl) u
405 t1))).(let H4 \def (eq_ind T (THead (Bind b) v t0) (\lambda (ee: T).(match ee
406 in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef
407 _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return
408 (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow
409 False])])) I (THead (Flat Appl) u t1) H3) in (False_ind (ex2 T (\lambda (t3:
410 T).(sty0 g c0 t1 t3)) (\lambda (t3: T).(eq T (THead (Bind b) v t2) (THead
411 (Flat Appl) u t3)))) H4)))))))))) (\lambda (c0: C).(\lambda (v: T).(\lambda
412 (t0: T).(\lambda (t2: T).(\lambda (H1: (sty0 g c0 t0 t2)).(\lambda (H2: (((eq
413 T t0 (THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g c0 t1 t3))
414 (\lambda (t3: T).(eq T t2 (THead (Flat Appl) u t3))))))).(\lambda (H3: (eq T
415 (THead (Flat Appl) v t0) (THead (Flat Appl) u t1))).(let H4 \def (f_equal T T
416 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
417 \Rightarrow v | (TLRef _) \Rightarrow v | (THead _ t _) \Rightarrow t]))
418 (THead (Flat Appl) v t0) (THead (Flat Appl) u t1) H3) in ((let H5 \def
419 (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with
420 [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t)
421 \Rightarrow t])) (THead (Flat Appl) v t0) (THead (Flat Appl) u t1) H3) in
422 (\lambda (H6: (eq T v u)).(let H7 \def (eq_ind T t0 (\lambda (t: T).((eq T t
423 (THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g c0 t1 t3))
424 (\lambda (t3: T).(eq T t2 (THead (Flat Appl) u t3)))))) H2 t1 H5) in (let H8
425 \def (eq_ind T t0 (\lambda (t: T).(sty0 g c0 t t2)) H1 t1 H5) in (eq_ind_r T
426 u (\lambda (t: T).(ex2 T (\lambda (t3: T).(sty0 g c0 t1 t3)) (\lambda (t3:
427 T).(eq T (THead (Flat Appl) t t2) (THead (Flat Appl) u t3))))) (ex_intro2 T
428 (\lambda (t3: T).(sty0 g c0 t1 t3)) (\lambda (t3: T).(eq T (THead (Flat Appl)
429 u t2) (THead (Flat Appl) u t3))) t2 H8 (refl_equal T (THead (Flat Appl) u
430 t2))) v H6))))) H4))))))))) (\lambda (c0: C).(\lambda (v1: T).(\lambda (v2:
431 T).(\lambda (_: (sty0 g c0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Flat Appl)
432 u t1)) \to (ex2 T (\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T
433 v2 (THead (Flat Appl) u t2))))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda
434 (_: (sty0 g c0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Flat Appl) u t1)) \to
435 (ex2 T (\lambda (t3: T).(sty0 g c0 t1 t3)) (\lambda (t3: T).(eq T t2 (THead
436 (Flat Appl) u t3))))))).(\lambda (H5: (eq T (THead (Flat Cast) v1 t0) (THead
437 (Flat Appl) u t1))).(let H6 \def (eq_ind T (THead (Flat Cast) v1 t0) (\lambda
438 (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
439 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
440 (match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False |
441 (Flat f) \Rightarrow (match f in F return (\lambda (_: F).Prop) with [Appl
442 \Rightarrow False | Cast \Rightarrow True])])])) I (THead (Flat Appl) u t1)
443 H5) in (False_ind (ex2 T (\lambda (t3: T).(sty0 g c0 t1 t3)) (\lambda (t3:
444 T).(eq T (THead (Flat Cast) v2 t2) (THead (Flat Appl) u t3)))) H6))))))))))))
450 theorem sty0_gen_cast:
451 \forall (g: G).(\forall (c: C).(\forall (v1: T).(\forall (t1: T).(\forall
452 (x: T).((sty0 g c (THead (Flat Cast) v1 t1) x) \to (ex3_2 T T (\lambda (v2:
453 T).(\lambda (_: T).(sty0 g c v1 v2))) (\lambda (_: T).(\lambda (t2: T).(sty0
454 g c t1 t2))) (\lambda (v2: T).(\lambda (t2: T).(eq T x (THead (Flat Cast) v2
457 \lambda (g: G).(\lambda (c: C).(\lambda (v1: T).(\lambda (t1: T).(\lambda
458 (x: T).(\lambda (H: (sty0 g c (THead (Flat Cast) v1 t1) x)).(insert_eq T
459 (THead (Flat Cast) v1 t1) (\lambda (t: T).(sty0 g c t x)) (\lambda (_:
460 T).(ex3_2 T T (\lambda (v2: T).(\lambda (_: T).(sty0 g c v1 v2))) (\lambda
461 (_: T).(\lambda (t2: T).(sty0 g c t1 t2))) (\lambda (v2: T).(\lambda (t2:
462 T).(eq T x (THead (Flat Cast) v2 t2)))))) (\lambda (y: T).(\lambda (H0: (sty0
463 g c y x)).(sty0_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).((eq
464 T t (THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v2: T).(\lambda (_:
465 T).(sty0 g c0 v1 v2))) (\lambda (_: T).(\lambda (t2: T).(sty0 g c0 t1 t2)))
466 (\lambda (v2: T).(\lambda (t2: T).(eq T t0 (THead (Flat Cast) v2 t2)))))))))
467 (\lambda (c0: C).(\lambda (n: nat).(\lambda (H1: (eq T (TSort n) (THead (Flat
468 Cast) v1 t1))).(let H2 \def (eq_ind T (TSort n) (\lambda (ee: T).(match ee in
469 T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _)
470 \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead (Flat Cast)
471 v1 t1) H1) in (False_ind (ex3_2 T T (\lambda (v2: T).(\lambda (_: T).(sty0 g
472 c0 v1 v2))) (\lambda (_: T).(\lambda (t2: T).(sty0 g c0 t1 t2))) (\lambda
473 (v2: T).(\lambda (t2: T).(eq T (TSort (next g n)) (THead (Flat Cast) v2
474 t2))))) H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i:
475 nat).(\lambda (_: (getl i c0 (CHead d (Bind Abbr) v))).(\lambda (w:
476 T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T v (THead (Flat Cast) v1
477 t1)) \to (ex3_2 T T (\lambda (v2: T).(\lambda (_: T).(sty0 g d v1 v2)))
478 (\lambda (_: T).(\lambda (t2: T).(sty0 g d t1 t2))) (\lambda (v2: T).(\lambda
479 (t2: T).(eq T w (THead (Flat Cast) v2 t2)))))))).(\lambda (H4: (eq T (TLRef
480 i) (THead (Flat Cast) v1 t1))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee:
481 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
482 False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
483 (THead (Flat Cast) v1 t1) H4) in (False_ind (ex3_2 T T (\lambda (v2:
484 T).(\lambda (_: T).(sty0 g c0 v1 v2))) (\lambda (_: T).(\lambda (t2: T).(sty0
485 g c0 t1 t2))) (\lambda (v2: T).(\lambda (t2: T).(eq T (lift (S i) O w) (THead
486 (Flat Cast) v2 t2))))) H5))))))))))) (\lambda (c0: C).(\lambda (d:
487 C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind
488 Abst) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T
489 v (THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v2: T).(\lambda (_:
490 T).(sty0 g d v1 v2))) (\lambda (_: T).(\lambda (t2: T).(sty0 g d t1 t2)))
491 (\lambda (v2: T).(\lambda (t2: T).(eq T w (THead (Flat Cast) v2
492 t2)))))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat Cast) v1 t1))).(let H5
493 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_:
494 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
495 (THead _ _ _) \Rightarrow False])) I (THead (Flat Cast) v1 t1) H4) in
496 (False_ind (ex3_2 T T (\lambda (v2: T).(\lambda (_: T).(sty0 g c0 v1 v2)))
497 (\lambda (_: T).(\lambda (t2: T).(sty0 g c0 t1 t2))) (\lambda (v2:
498 T).(\lambda (t2: T).(eq T (lift (S i) O v) (THead (Flat Cast) v2 t2)))))
499 H5))))))))))) (\lambda (b: B).(\lambda (c0: C).(\lambda (v: T).(\lambda (t0:
500 T).(\lambda (t2: T).(\lambda (_: (sty0 g (CHead c0 (Bind b) v) t0
501 t2)).(\lambda (_: (((eq T t0 (THead (Flat Cast) v1 t1)) \to (ex3_2 T T
502 (\lambda (v2: T).(\lambda (_: T).(sty0 g (CHead c0 (Bind b) v) v1 v2)))
503 (\lambda (_: T).(\lambda (t3: T).(sty0 g (CHead c0 (Bind b) v) t1 t3)))
504 (\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) v2
505 t3)))))))).(\lambda (H3: (eq T (THead (Bind b) v t0) (THead (Flat Cast) v1
506 t1))).(let H4 \def (eq_ind T (THead (Bind b) v t0) (\lambda (ee: T).(match ee
507 in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef
508 _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return
509 (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow
510 False])])) I (THead (Flat Cast) v1 t1) H3) in (False_ind (ex3_2 T T (\lambda
511 (v2: T).(\lambda (_: T).(sty0 g c0 v1 v2))) (\lambda (_: T).(\lambda (t3:
512 T).(sty0 g c0 t1 t3))) (\lambda (v2: T).(\lambda (t3: T).(eq T (THead (Bind
513 b) v t2) (THead (Flat Cast) v2 t3))))) H4)))))))))) (\lambda (c0: C).(\lambda
514 (v: T).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (sty0 g c0 t0
515 t2)).(\lambda (_: (((eq T t0 (THead (Flat Cast) v1 t1)) \to (ex3_2 T T
516 (\lambda (v2: T).(\lambda (_: T).(sty0 g c0 v1 v2))) (\lambda (_: T).(\lambda
517 (t3: T).(sty0 g c0 t1 t3))) (\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead
518 (Flat Cast) v2 t3)))))))).(\lambda (H3: (eq T (THead (Flat Appl) v t0) (THead
519 (Flat Cast) v1 t1))).(let H4 \def (eq_ind T (THead (Flat Appl) v t0) (\lambda
520 (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
521 \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
522 (match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False |
523 (Flat f) \Rightarrow (match f in F return (\lambda (_: F).Prop) with [Appl
524 \Rightarrow True | Cast \Rightarrow False])])])) I (THead (Flat Cast) v1 t1)
525 H3) in (False_ind (ex3_2 T T (\lambda (v2: T).(\lambda (_: T).(sty0 g c0 v1
526 v2))) (\lambda (_: T).(\lambda (t3: T).(sty0 g c0 t1 t3))) (\lambda (v2:
527 T).(\lambda (t3: T).(eq T (THead (Flat Appl) v t2) (THead (Flat Cast) v2
528 t3))))) H4))))))))) (\lambda (c0: C).(\lambda (v0: T).(\lambda (v2:
529 T).(\lambda (H1: (sty0 g c0 v0 v2)).(\lambda (H2: (((eq T v0 (THead (Flat
530 Cast) v1 t1)) \to (ex3_2 T T (\lambda (v3: T).(\lambda (_: T).(sty0 g c0 v1
531 v3))) (\lambda (_: T).(\lambda (t2: T).(sty0 g c0 t1 t2))) (\lambda (v3:
532 T).(\lambda (t2: T).(eq T v2 (THead (Flat Cast) v3 t2)))))))).(\lambda (t0:
533 T).(\lambda (t2: T).(\lambda (H3: (sty0 g c0 t0 t2)).(\lambda (H4: (((eq T t0
534 (THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v3: T).(\lambda (_:
535 T).(sty0 g c0 v1 v3))) (\lambda (_: T).(\lambda (t3: T).(sty0 g c0 t1 t3)))
536 (\lambda (v3: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) v3
537 t3)))))))).(\lambda (H5: (eq T (THead (Flat Cast) v0 t0) (THead (Flat Cast)
538 v1 t1))).(let H6 \def (f_equal T T (\lambda (e: T).(match e in T return
539 (\lambda (_: T).T) with [(TSort _) \Rightarrow v0 | (TLRef _) \Rightarrow v0
540 | (THead _ t _) \Rightarrow t])) (THead (Flat Cast) v0 t0) (THead (Flat Cast)
541 v1 t1) H5) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e in T return
542 (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0
543 | (THead _ _ t) \Rightarrow t])) (THead (Flat Cast) v0 t0) (THead (Flat Cast)
544 v1 t1) H5) in (\lambda (H8: (eq T v0 v1)).(let H9 \def (eq_ind T t0 (\lambda
545 (t: T).((eq T t (THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v3:
546 T).(\lambda (_: T).(sty0 g c0 v1 v3))) (\lambda (_: T).(\lambda (t3: T).(sty0
547 g c0 t1 t3))) (\lambda (v3: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast)
548 v3 t3))))))) H4 t1 H7) in (let H10 \def (eq_ind T t0 (\lambda (t: T).(sty0 g
549 c0 t t2)) H3 t1 H7) in (let H11 \def (eq_ind T v0 (\lambda (t: T).((eq T t
550 (THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v3: T).(\lambda (_:
551 T).(sty0 g c0 v1 v3))) (\lambda (_: T).(\lambda (t3: T).(sty0 g c0 t1 t3)))
552 (\lambda (v3: T).(\lambda (t3: T).(eq T v2 (THead (Flat Cast) v3 t3))))))) H2
553 v1 H8) in (let H12 \def (eq_ind T v0 (\lambda (t: T).(sty0 g c0 t v2)) H1 v1
554 H8) in (ex3_2_intro T T (\lambda (v3: T).(\lambda (_: T).(sty0 g c0 v1 v3)))
555 (\lambda (_: T).(\lambda (t3: T).(sty0 g c0 t1 t3))) (\lambda (v3:
556 T).(\lambda (t3: T).(eq T (THead (Flat Cast) v2 t2) (THead (Flat Cast) v3
557 t3)))) v2 t2 H12 H10 (refl_equal T (THead (Flat Cast) v2 t2)))))))))
558 H6)))))))))))) c y x H0))) H)))))).