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