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