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