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 set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd".
19 include "ty3/defs.ma".
21 include "pc3/props.ma".
24 \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((ty3 g c
25 (TSort n) x) \to (pc3 c (TSort (next g n)) x)))))
27 \lambda (g: G).(\lambda (c: C).(\lambda (x: T).(\lambda (n: nat).(\lambda
28 (H: (ty3 g c (TSort n) x)).(insert_eq T (TSort n) (\lambda (t: T).(ty3 g c t
29 x)) (pc3 c (TSort (next g n)) x) (\lambda (y: T).(\lambda (H0: (ty3 g c y
30 x)).(ty3_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).((eq T t
31 (TSort n)) \to (pc3 c0 (TSort (next g n)) t0))))) (\lambda (c0: C).(\lambda
32 (t2: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 t2 t)).(\lambda (_: (((eq T t2
33 (TSort n)) \to (pc3 c0 (TSort (next g n)) t)))).(\lambda (u: T).(\lambda (t1:
34 T).(\lambda (H3: (ty3 g c0 u t1)).(\lambda (H4: (((eq T u (TSort n)) \to (pc3
35 c0 (TSort (next g n)) t1)))).(\lambda (H5: (pc3 c0 t1 t2)).(\lambda (H6: (eq
36 T u (TSort n))).(let H7 \def (f_equal T T (\lambda (e: T).e) u (TSort n) H6)
37 in (let H8 \def (eq_ind T u (\lambda (t0: T).((eq T t0 (TSort n)) \to (pc3 c0
38 (TSort (next g n)) t1))) H4 (TSort n) H7) in (let H9 \def (eq_ind T u
39 (\lambda (t0: T).(ty3 g c0 t0 t1)) H3 (TSort n) H7) in (pc3_t t1 c0 (TSort
40 (next g n)) (H8 (refl_equal T (TSort n))) t2 H5))))))))))))))) (\lambda (c0:
41 C).(\lambda (m: nat).(\lambda (H1: (eq T (TSort m) (TSort n))).(let H2 \def
42 (f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with
43 [(TSort n0) \Rightarrow n0 | (TLRef _) \Rightarrow m | (THead _ _ _)
44 \Rightarrow m])) (TSort m) (TSort n) H1) in (eq_ind_r nat n (\lambda (n0:
45 nat).(pc3 c0 (TSort (next g n)) (TSort (next g n0)))) (pc3_refl c0 (TSort
46 (next g n))) m H2))))) (\lambda (n0: nat).(\lambda (c0: C).(\lambda (d:
47 C).(\lambda (u: T).(\lambda (_: (getl n0 c0 (CHead d (Bind Abbr)
48 u))).(\lambda (t: T).(\lambda (_: (ty3 g d u t)).(\lambda (_: (((eq T u
49 (TSort n)) \to (pc3 d (TSort (next g n)) t)))).(\lambda (H4: (eq T (TLRef n0)
50 (TSort n))).(let H5 \def (eq_ind T (TLRef n0) (\lambda (ee: T).(match ee in T
51 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
52 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n) H4) in
53 (False_ind (pc3 c0 (TSort (next g n)) (lift (S n0) O t)) H5)))))))))))
54 (\lambda (n0: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda
55 (_: (getl n0 c0 (CHead d (Bind Abst) u))).(\lambda (t: T).(\lambda (_: (ty3 g
56 d u t)).(\lambda (_: (((eq T u (TSort n)) \to (pc3 d (TSort (next g n))
57 t)))).(\lambda (H4: (eq T (TLRef n0) (TSort n))).(let H5 \def (eq_ind T
58 (TLRef n0) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with
59 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _)
60 \Rightarrow False])) I (TSort n) H4) in (False_ind (pc3 c0 (TSort (next g n))
61 (lift (S n0) O u)) H5))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda
62 (t: T).(\lambda (_: (ty3 g c0 u t)).(\lambda (_: (((eq T u (TSort n)) \to
63 (pc3 c0 (TSort (next g n)) t)))).(\lambda (b: B).(\lambda (t1: T).(\lambda
64 (t2: T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t1 t2)).(\lambda (_: (((eq
65 T t1 (TSort n)) \to (pc3 (CHead c0 (Bind b) u) (TSort (next g n))
66 t2)))).(\lambda (t0: T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t2
67 t0)).(\lambda (_: (((eq T t2 (TSort n)) \to (pc3 (CHead c0 (Bind b) u) (TSort
68 (next g n)) t0)))).(\lambda (H7: (eq T (THead (Bind b) u t1) (TSort n))).(let
69 H8 \def (eq_ind T (THead (Bind b) u t1) (\lambda (ee: T).(match ee in T
70 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
71 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H7) in
72 (False_ind (pc3 c0 (TSort (next g n)) (THead (Bind b) u t2))
73 H8)))))))))))))))) (\lambda (c0: C).(\lambda (w: T).(\lambda (u: T).(\lambda
74 (_: (ty3 g c0 w u)).(\lambda (_: (((eq T w (TSort n)) \to (pc3 c0 (TSort
75 (next g n)) u)))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 v
76 (THead (Bind Abst) u t))).(\lambda (_: (((eq T v (TSort n)) \to (pc3 c0
77 (TSort (next g n)) (THead (Bind Abst) u t))))).(\lambda (H5: (eq T (THead
78 (Flat Appl) w v) (TSort n))).(let H6 \def (eq_ind T (THead (Flat Appl) w v)
79 (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
80 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
81 True])) I (TSort n) H5) in (False_ind (pc3 c0 (TSort (next g n)) (THead (Flat
82 Appl) w (THead (Bind Abst) u t))) H6)))))))))))) (\lambda (c0: C).(\lambda
83 (t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g c0 t1 t2)).(\lambda (_: (((eq T
84 t1 (TSort n)) \to (pc3 c0 (TSort (next g n)) t2)))).(\lambda (t0: T).(\lambda
85 (_: (ty3 g c0 t2 t0)).(\lambda (_: (((eq T t2 (TSort n)) \to (pc3 c0 (TSort
86 (next g n)) t0)))).(\lambda (H5: (eq T (THead (Flat Cast) t2 t1) (TSort
87 n))).(let H6 \def (eq_ind T (THead (Flat Cast) t2 t1) (\lambda (ee: T).(match
88 ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False |
89 (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n)
90 H5) in (False_ind (pc3 c0 (TSort (next g n)) (THead (Flat Cast) t0 t2))
91 H6))))))))))) c y x H0))) H))))).
94 \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((ty3 g c
95 (TLRef n) x) \to (or (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda
96 (t: T).(pc3 c (lift (S n) O t) x)))) (\lambda (e: C).(\lambda (u: T).(\lambda
97 (_: T).(getl n c (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
98 T).(\lambda (t: T).(ty3 g e u t))))) (ex3_3 C T T (\lambda (_: C).(\lambda
99 (u: T).(\lambda (_: T).(pc3 c (lift (S n) O u) x)))) (\lambda (e: C).(\lambda
100 (u: T).(\lambda (_: T).(getl n c (CHead e (Bind Abst) u))))) (\lambda (e:
101 C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t))))))))))
103 \lambda (g: G).(\lambda (c: C).(\lambda (x: T).(\lambda (n: nat).(\lambda
104 (H: (ty3 g c (TLRef n) x)).(insert_eq T (TLRef n) (\lambda (t: T).(ty3 g c t
105 x)) (or (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 c
106 (lift (S n) O t) x)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl
107 n c (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t:
108 T).(ty3 g e u t))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u: T).(\lambda
109 (_: T).(pc3 c (lift (S n) O u) x)))) (\lambda (e: C).(\lambda (u: T).(\lambda
110 (_: T).(getl n c (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u:
111 T).(\lambda (t: T).(ty3 g e u t)))))) (\lambda (y: T).(\lambda (H0: (ty3 g c
112 y x)).(ty3_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).((eq T t
113 (TLRef n)) \to (or (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t1:
114 T).(pc3 c0 (lift (S n) O t1) t0)))) (\lambda (e: C).(\lambda (u: T).(\lambda
115 (_: T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
116 T).(\lambda (t1: T).(ty3 g e u t1))))) (ex3_3 C T T (\lambda (_: C).(\lambda
117 (u: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u) t0)))) (\lambda (e:
118 C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u)))))
119 (\lambda (e: C).(\lambda (u: T).(\lambda (t1: T).(ty3 g e u t1))))))))))
120 (\lambda (c0: C).(\lambda (t2: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 t2
121 t)).(\lambda (_: (((eq T t2 (TLRef n)) \to (or (ex3_3 C T T (\lambda (_:
122 C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t)))) (\lambda
123 (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u)))))
124 (\lambda (e: C).(\lambda (u: T).(\lambda (t0: T).(ty3 g e u t0))))) (ex3_3 C
125 T T (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u)
126 t)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e
127 (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t0: T).(ty3 g e
128 u 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 (t0:
314 T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t2 t0)).(\lambda (_: (((eq T t2
315 (TLRef n)) \to (or (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t3:
316 T).(pc3 (CHead c0 (Bind b) u) (lift (S n) O t3) t0)))) (\lambda (e:
317 C).(\lambda (u0: T).(\lambda (_: T).(getl n (CHead c0 (Bind b) u) (CHead e
318 (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t3: T).(ty3 g
319 e u0 t3))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_:
320 T).(pc3 (CHead c0 (Bind b) u) (lift (S n) O u0) t0)))) (\lambda (e:
321 C).(\lambda (u0: T).(\lambda (_: T).(getl n (CHead c0 (Bind b) u) (CHead e
322 (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t3: T).(ty3 g
323 e u0 t3))))))))).(\lambda (H7: (eq T (THead (Bind b) u t1) (TLRef n))).(let
324 H8 \def (eq_ind T (THead (Bind b) u t1) (\lambda (ee: T).(match ee in T
325 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
326 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H7) in
327 (False_ind (or (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t3:
328 T).(pc3 c0 (lift (S n) O t3) (THead (Bind b) u t2))))) (\lambda (e:
329 C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u0)))))
330 (\lambda (e: C).(\lambda (u0: T).(\lambda (t3: T).(ty3 g e u0 t3))))) (ex3_3
331 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 c0 (lift (S n) O
332 u0) (THead (Bind b) u t2))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
333 T).(getl n c0 (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0:
334 T).(\lambda (t3: T).(ty3 g e u0 t3)))))) H8)))))))))))))))) (\lambda (c0:
335 C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 g c0 w u)).(\lambda (_:
336 (((eq T w (TLRef n)) \to (or (ex3_3 C T T (\lambda (_: C).(\lambda (_:
337 T).(\lambda (t: T).(pc3 c0 (lift (S n) O t) u)))) (\lambda (e: C).(\lambda
338 (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u0))))) (\lambda (e:
339 C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) (ex3_3 C T T (\lambda
340 (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u0) u))))
341 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
342 Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0
343 t))))))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 v (THead
344 (Bind Abst) u t))).(\lambda (_: (((eq T v (TLRef n)) \to (or (ex3_3 C T T
345 (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0)
346 (THead (Bind Abst) u t))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_:
347 T).(getl n c0 (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0:
348 T).(\lambda (t0: T).(ty3 g e u0 t0))))) (ex3_3 C T T (\lambda (_: C).(\lambda
349 (u0: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u0) (THead (Bind Abst) u t)))))
350 (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
351 Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g e u0
352 t0))))))))).(\lambda (H5: (eq T (THead (Flat Appl) w v) (TLRef n))).(let H6
353 \def (eq_ind T (THead (Flat Appl) w v) (\lambda (ee: T).(match ee in T return
354 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
355 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H5) in
356 (False_ind (or (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0:
357 T).(pc3 c0 (lift (S n) O t0) (THead (Flat Appl) w (THead (Bind Abst) u
358 t)))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e
359 (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g
360 e u0 t0))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_:
361 T).(pc3 c0 (lift (S n) O u0) (THead (Flat Appl) w (THead (Bind Abst) u
362 t)))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl n c0 (CHead e
363 (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t0: T).(ty3 g
364 e u0 t0)))))) H6)))))))))))) (\lambda (c0: C).(\lambda (t1: T).(\lambda (t2:
365 T).(\lambda (_: (ty3 g c0 t1 t2)).(\lambda (_: (((eq T t1 (TLRef n)) \to (or
366 (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 c0 (lift (S
367 n) O t) t2)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0
368 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t:
369 T).(ty3 g e u t))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u: T).(\lambda
370 (_: T).(pc3 c0 (lift (S n) O u) t2)))) (\lambda (e: C).(\lambda (u:
371 T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e:
372 C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t))))))))).(\lambda (t0:
373 T).(\lambda (_: (ty3 g c0 t2 t0)).(\lambda (_: (((eq T t2 (TLRef n)) \to (or
374 (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 c0 (lift (S
375 n) O t) t0)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0
376 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t:
377 T).(ty3 g e u t))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u: T).(\lambda
378 (_: T).(pc3 c0 (lift (S n) O u) t0)))) (\lambda (e: C).(\lambda (u:
379 T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e:
380 C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t))))))))).(\lambda (H5: (eq T
381 (THead (Flat Cast) t2 t1) (TLRef n))).(let H6 \def (eq_ind T (THead (Flat
382 Cast) t2 t1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop)
383 with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _
384 _) \Rightarrow True])) I (TLRef n) H5) in (False_ind (or (ex3_3 C T T
385 (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 c0 (lift (S n) O t)
386 (THead (Flat Cast) t0 t2))))) (\lambda (e: C).(\lambda (u: T).(\lambda (_:
387 T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
388 T).(\lambda (t: T).(ty3 g e u t))))) (ex3_3 C T T (\lambda (_: C).(\lambda
389 (u: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u) (THead (Flat Cast) t0 t2)))))
390 (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind
391 Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u
392 t)))))) H6))))))))))) c y x H0))) H))))).
394 theorem ty3_gen_bind:
395 \forall (g: G).(\forall (b: B).(\forall (c: C).(\forall (u: T).(\forall (t1:
396 T).(\forall (x: T).((ty3 g c (THead (Bind b) u t1) x) \to (ex4_3 T T T
397 (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 c (THead (Bind b) u t2)
398 x)))) (\lambda (_: T).(\lambda (t: T).(\lambda (_: T).(ty3 g c u t))))
399 (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c (Bind b) u)
400 t1 t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t0: T).(ty3 g (CHead c
401 (Bind b) u) t2 t0)))))))))))
403 \lambda (g: G).(\lambda (b: B).(\lambda (c: C).(\lambda (u: T).(\lambda (t1:
404 T).(\lambda (x: T).(\lambda (H: (ty3 g c (THead (Bind b) u t1) x)).(insert_eq
405 T (THead (Bind b) u t1) (\lambda (t: T).(ty3 g c t x)) (ex4_3 T T T (\lambda
406 (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 c (THead (Bind b) u t2) x))))
407 (\lambda (_: T).(\lambda (t: T).(\lambda (_: T).(ty3 g c u t)))) (\lambda
408 (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c (Bind b) u) t1 t2))))
409 (\lambda (t2: T).(\lambda (_: T).(\lambda (t0: T).(ty3 g (CHead c (Bind b) u)
410 t2 t0))))) (\lambda (y: T).(\lambda (H0: (ty3 g c y x)).(ty3_ind g (\lambda
411 (c0: C).(\lambda (t: T).(\lambda (t0: T).((eq T t (THead (Bind b) u t1)) \to
412 (ex4_3 T T T (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead
413 (Bind b) u t2) t0)))) (\lambda (_: T).(\lambda (t3: T).(\lambda (_: T).(ty3 g
414 c0 u t3)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0
415 (Bind b) u) t1 t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t4: T).(ty3
416 g (CHead c0 (Bind b) u) t2 t4))))))))) (\lambda (c0: C).(\lambda (t2:
417 T).(\lambda (t: T).(\lambda (_: (ty3 g c0 t2 t)).(\lambda (_: (((eq T t2
418 (THead (Bind b) u t1)) \to (ex4_3 T T T (\lambda (t3: T).(\lambda (_:
419 T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t3) t)))) (\lambda (_:
420 T).(\lambda (t0: T).(\lambda (_: T).(ty3 g c0 u t0)))) (\lambda (t3:
421 T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t3))))
422 (\lambda (t3: T).(\lambda (_: T).(\lambda (t4: T).(ty3 g (CHead c0 (Bind b)
423 u) t3 t4)))))))).(\lambda (u0: T).(\lambda (t0: T).(\lambda (H3: (ty3 g c0 u0
424 t0)).(\lambda (H4: (((eq T u0 (THead (Bind b) u t1)) \to (ex4_3 T T T
425 (\lambda (t3: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u
426 t3) t0)))) (\lambda (_: T).(\lambda (t4: T).(\lambda (_: T).(ty3 g c0 u
427 t4)))) (\lambda (t3: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0
428 (Bind b) u) t1 t3)))) (\lambda (t3: T).(\lambda (_: T).(\lambda (t5: T).(ty3
429 g (CHead c0 (Bind b) u) t3 t5)))))))).(\lambda (H5: (pc3 c0 t0 t2)).(\lambda
430 (H6: (eq T u0 (THead (Bind b) u t1))).(let H7 \def (f_equal T T (\lambda (e:
431 T).e) u0 (THead (Bind b) u t1) H6) in (let H8 \def (eq_ind T u0 (\lambda (t3:
432 T).((eq T t3 (THead (Bind b) u t1)) \to (ex4_3 T T T (\lambda (t4:
433 T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t4) t0))))
434 (\lambda (_: T).(\lambda (t5: T).(\lambda (_: T).(ty3 g c0 u t5)))) (\lambda
435 (t4: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1
436 t4)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (t6: T).(ty3 g (CHead c0
437 (Bind b) u) t4 t6))))))) H4 (THead (Bind b) u t1) H7) in (let H9 \def (eq_ind
438 T u0 (\lambda (t3: T).(ty3 g c0 t3 t0)) H3 (THead (Bind b) u t1) H7) in (let
439 H10 \def (H8 (refl_equal T (THead (Bind b) u t1))) in (ex4_3_ind T T T
440 (\lambda (t3: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u
441 t3) t0)))) (\lambda (_: T).(\lambda (t4: T).(\lambda (_: T).(ty3 g c0 u
442 t4)))) (\lambda (t3: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0
443 (Bind b) u) t1 t3)))) (\lambda (t3: T).(\lambda (_: T).(\lambda (t5: T).(ty3
444 g (CHead c0 (Bind b) u) t3 t5)))) (ex4_3 T T T (\lambda (t3: T).(\lambda (_:
445 T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t3) t2)))) (\lambda (_:
446 T).(\lambda (t4: T).(\lambda (_: T).(ty3 g c0 u t4)))) (\lambda (t3:
447 T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t3))))
448 (\lambda (t3: T).(\lambda (_: T).(\lambda (t5: T).(ty3 g (CHead c0 (Bind b)
449 u) t3 t5))))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (x2: T).(\lambda
450 (H11: (pc3 c0 (THead (Bind b) u x0) t0)).(\lambda (H12: (ty3 g c0 u
451 x1)).(\lambda (H13: (ty3 g (CHead c0 (Bind b) u) t1 x0)).(\lambda (H14: (ty3
452 g (CHead c0 (Bind b) u) x0 x2)).(ex4_3_intro T T T (\lambda (t3: T).(\lambda
453 (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t3) t2)))) (\lambda (_:
454 T).(\lambda (t4: T).(\lambda (_: T).(ty3 g c0 u t4)))) (\lambda (t3:
455 T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t3))))
456 (\lambda (t3: T).(\lambda (_: T).(\lambda (t5: T).(ty3 g (CHead c0 (Bind b)
457 u) t3 t5)))) x0 x1 x2 (pc3_t t0 c0 (THead (Bind b) u x0) H11 t2 H5) H12 H13
458 H14)))))))) H10)))))))))))))))) (\lambda (c0: C).(\lambda (m: nat).(\lambda
459 (H1: (eq T (TSort m) (THead (Bind b) u t1))).(let H2 \def (eq_ind T (TSort m)
460 (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
461 \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
462 False])) I (THead (Bind b) u t1) H1) in (False_ind (ex4_3 T T T (\lambda (t2:
463 T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t2) (TSort (next
464 g m)))))) (\lambda (_: T).(\lambda (t: T).(\lambda (_: T).(ty3 g c0 u t))))
465 (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u)
466 t1 t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t0: T).(ty3 g (CHead c0
467 (Bind b) u) t2 t0))))) H2))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda
468 (d: C).(\lambda (u0: T).(\lambda (_: (getl n c0 (CHead d (Bind Abbr)
469 u0))).(\lambda (t: T).(\lambda (_: (ty3 g d u0 t)).(\lambda (_: (((eq T u0
470 (THead (Bind b) u t1)) \to (ex4_3 T T T (\lambda (t2: T).(\lambda (_:
471 T).(\lambda (_: T).(pc3 d (THead (Bind b) u t2) t)))) (\lambda (_:
472 T).(\lambda (t0: T).(\lambda (_: T).(ty3 g d u t0)))) (\lambda (t2:
473 T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead d (Bind b) u) t1 t2))))
474 (\lambda (t2: T).(\lambda (_: T).(\lambda (t3: T).(ty3 g (CHead d (Bind b) u)
475 t2 t3)))))))).(\lambda (H4: (eq T (TLRef n) (THead (Bind b) u t1))).(let H5
476 \def (eq_ind T (TLRef n) (\lambda (ee: T).(match ee in T return (\lambda (_:
477 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
478 (THead _ _ _) \Rightarrow False])) I (THead (Bind b) u t1) H4) in (False_ind
479 (ex4_3 T T T (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead
480 (Bind b) u t2) (lift (S n) O t))))) (\lambda (_: T).(\lambda (t0: T).(\lambda
481 (_: T).(ty3 g c0 u t0)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (_:
482 T).(ty3 g (CHead c0 (Bind b) u) t1 t2)))) (\lambda (t2: T).(\lambda (_:
483 T).(\lambda (t3: T).(ty3 g (CHead c0 (Bind b) u) t2 t3))))) H5)))))))))))
484 (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda
485 (_: (getl n c0 (CHead d (Bind Abst) u0))).(\lambda (t: T).(\lambda (_: (ty3 g
486 d u0 t)).(\lambda (_: (((eq T u0 (THead (Bind b) u t1)) \to (ex4_3 T T T
487 (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 d (THead (Bind b) u t2)
488 t)))) (\lambda (_: T).(\lambda (t0: T).(\lambda (_: T).(ty3 g d u t0))))
489 (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead d (Bind b) u)
490 t1 t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t3: T).(ty3 g (CHead d
491 (Bind b) u) t2 t3)))))))).(\lambda (H4: (eq T (TLRef n) (THead (Bind b) u
492 t1))).(let H5 \def (eq_ind T (TLRef n) (\lambda (ee: T).(match ee in T return
493 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
494 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Bind b) u t1)
495 H4) in (False_ind (ex4_3 T T T (\lambda (t2: T).(\lambda (_: T).(\lambda (_:
496 T).(pc3 c0 (THead (Bind b) u t2) (lift (S n) O u0))))) (\lambda (_:
497 T).(\lambda (t0: T).(\lambda (_: T).(ty3 g c0 u t0)))) (\lambda (t2:
498 T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t2))))
499 (\lambda (t2: T).(\lambda (_: T).(\lambda (t3: T).(ty3 g (CHead c0 (Bind b)
500 u) t2 t3))))) H5))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda (t:
501 T).(\lambda (H1: (ty3 g c0 u0 t)).(\lambda (H2: (((eq T u0 (THead (Bind b) u
502 t1)) \to (ex4_3 T T T (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3
503 c0 (THead (Bind b) u t2) t)))) (\lambda (_: T).(\lambda (t0: T).(\lambda (_:
504 T).(ty3 g c0 u t0)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g
505 (CHead c0 (Bind b) u) t1 t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda
506 (t3: T).(ty3 g (CHead c0 (Bind b) u) t2 t3)))))))).(\lambda (b0: B).(\lambda
507 (t0: T).(\lambda (t2: T).(\lambda (H3: (ty3 g (CHead c0 (Bind b0) u0) t0
508 t2)).(\lambda (H4: (((eq T t0 (THead (Bind b) u t1)) \to (ex4_3 T T T
509 (\lambda (t3: T).(\lambda (_: T).(\lambda (_: T).(pc3 (CHead c0 (Bind b0) u0)
510 (THead (Bind b) u t3) t2)))) (\lambda (_: T).(\lambda (t4: T).(\lambda (_:
511 T).(ty3 g (CHead c0 (Bind b0) u0) u t4)))) (\lambda (t3: T).(\lambda (_:
512 T).(\lambda (_: T).(ty3 g (CHead (CHead c0 (Bind b0) u0) (Bind b) u) t1
513 t3)))) (\lambda (t3: T).(\lambda (_: T).(\lambda (t5: T).(ty3 g (CHead (CHead
514 c0 (Bind b0) u0) (Bind b) u) t3 t5)))))))).(\lambda (t3: T).(\lambda (H5:
515 (ty3 g (CHead c0 (Bind b0) u0) t2 t3)).(\lambda (H6: (((eq T t2 (THead (Bind
516 b) u t1)) \to (ex4_3 T T T (\lambda (t4: T).(\lambda (_: T).(\lambda (_:
517 T).(pc3 (CHead c0 (Bind b0) u0) (THead (Bind b) u t4) t3)))) (\lambda (_:
518 T).(\lambda (t5: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b0) u0) u t5))))
519 (\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead (CHead c0
520 (Bind b0) u0) (Bind b) u) t1 t4)))) (\lambda (t4: T).(\lambda (_: T).(\lambda
521 (t6: T).(ty3 g (CHead (CHead c0 (Bind b0) u0) (Bind b) u) t4
522 t6)))))))).(\lambda (H7: (eq T (THead (Bind b0) u0 t0) (THead (Bind b) u
523 t1))).(let H8 \def (f_equal T B (\lambda (e: T).(match e in T return (\lambda
524 (_: T).B) with [(TSort _) \Rightarrow b0 | (TLRef _) \Rightarrow b0 | (THead
525 k _ _) \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b1)
526 \Rightarrow b1 | (Flat _) \Rightarrow b0])])) (THead (Bind b0) u0 t0) (THead
527 (Bind b) u t1) H7) in ((let H9 \def (f_equal T T (\lambda (e: T).(match e in
528 T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u0 | (TLRef _)
529 \Rightarrow u0 | (THead _ t4 _) \Rightarrow t4])) (THead (Bind b0) u0 t0)
530 (THead (Bind b) u t1) H7) in ((let H10 \def (f_equal T T (\lambda (e:
531 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 |
532 (TLRef _) \Rightarrow t0 | (THead _ _ t4) \Rightarrow t4])) (THead (Bind b0)
533 u0 t0) (THead (Bind b) u t1) H7) in (\lambda (H11: (eq T u0 u)).(\lambda
534 (H12: (eq B b0 b)).(let H13 \def (eq_ind T t0 (\lambda (t4: T).((eq T t4
535 (THead (Bind b) u t1)) \to (ex4_3 T T T (\lambda (t5: T).(\lambda (_:
536 T).(\lambda (_: T).(pc3 (CHead c0 (Bind b0) u0) (THead (Bind b) u t5) t2))))
537 (\lambda (_: T).(\lambda (t6: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b0)
538 u0) u t6)))) (\lambda (t5: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead
539 (CHead c0 (Bind b0) u0) (Bind b) u) t1 t5)))) (\lambda (t5: T).(\lambda (_:
540 T).(\lambda (t7: T).(ty3 g (CHead (CHead c0 (Bind b0) u0) (Bind b) u) t5
541 t7))))))) H4 t1 H10) in (let H14 \def (eq_ind T t0 (\lambda (t4: T).(ty3 g
542 (CHead c0 (Bind b0) u0) t4 t2)) H3 t1 H10) in (let H15 \def (eq_ind B b0
543 (\lambda (b1: B).((eq T t2 (THead (Bind b) u t1)) \to (ex4_3 T T T (\lambda
544 (t4: T).(\lambda (_: T).(\lambda (_: T).(pc3 (CHead c0 (Bind b1) u0) (THead
545 (Bind b) u t4) t3)))) (\lambda (_: T).(\lambda (t5: T).(\lambda (_: T).(ty3 g
546 (CHead c0 (Bind b1) u0) u t5)))) (\lambda (t4: T).(\lambda (_: T).(\lambda
547 (_: T).(ty3 g (CHead (CHead c0 (Bind b1) u0) (Bind b) u) t1 t4)))) (\lambda
548 (t4: T).(\lambda (_: T).(\lambda (t6: T).(ty3 g (CHead (CHead c0 (Bind b1)
549 u0) (Bind b) u) t4 t6))))))) H6 b H12) in (let H16 \def (eq_ind B b0 (\lambda
550 (b1: B).(ty3 g (CHead c0 (Bind b1) u0) t2 t3)) H5 b H12) in (let H17 \def
551 (eq_ind B b0 (\lambda (b1: B).((eq T t1 (THead (Bind b) u t1)) \to (ex4_3 T T
552 T (\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(pc3 (CHead c0 (Bind b1)
553 u0) (THead (Bind b) u t4) t2)))) (\lambda (_: T).(\lambda (t5: T).(\lambda
554 (_: T).(ty3 g (CHead c0 (Bind b1) u0) u t5)))) (\lambda (t4: T).(\lambda (_:
555 T).(\lambda (_: T).(ty3 g (CHead (CHead c0 (Bind b1) u0) (Bind b) u) t1
556 t4)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (t6: T).(ty3 g (CHead (CHead
557 c0 (Bind b1) u0) (Bind b) u) t4 t6))))))) H13 b H12) in (let H18 \def (eq_ind
558 B b0 (\lambda (b1: B).(ty3 g (CHead c0 (Bind b1) u0) t1 t2)) H14 b H12) in
559 (eq_ind_r B b (\lambda (b1: B).(ex4_3 T T T (\lambda (t4: T).(\lambda (_:
560 T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u t4) (THead (Bind b1) u0 t2)))))
561 (\lambda (_: T).(\lambda (t5: T).(\lambda (_: T).(ty3 g c0 u t5)))) (\lambda
562 (t4: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1
563 t4)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (t6: T).(ty3 g (CHead c0
564 (Bind b) u) t4 t6)))))) (let H19 \def (eq_ind T u0 (\lambda (t4: T).((eq T t2
565 (THead (Bind b) u t1)) \to (ex4_3 T T T (\lambda (t5: T).(\lambda (_:
566 T).(\lambda (_: T).(pc3 (CHead c0 (Bind b) t4) (THead (Bind b) u t5) t3))))
567 (\lambda (_: T).(\lambda (t6: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b)
568 t4) u t6)))) (\lambda (t5: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead
569 (CHead c0 (Bind b) t4) (Bind b) u) t1 t5)))) (\lambda (t5: T).(\lambda (_:
570 T).(\lambda (t7: T).(ty3 g (CHead (CHead c0 (Bind b) t4) (Bind b) u) t5
571 t7))))))) H15 u H11) in (let H20 \def (eq_ind T u0 (\lambda (t4: T).(ty3 g
572 (CHead c0 (Bind b) t4) t2 t3)) H16 u H11) in (let H21 \def (eq_ind T u0
573 (\lambda (t4: T).((eq T t1 (THead (Bind b) u t1)) \to (ex4_3 T T T (\lambda
574 (t5: T).(\lambda (_: T).(\lambda (_: T).(pc3 (CHead c0 (Bind b) t4) (THead
575 (Bind b) u t5) t2)))) (\lambda (_: T).(\lambda (t6: T).(\lambda (_: T).(ty3 g
576 (CHead c0 (Bind b) t4) u t6)))) (\lambda (t5: T).(\lambda (_: T).(\lambda (_:
577 T).(ty3 g (CHead (CHead c0 (Bind b) t4) (Bind b) u) t1 t5)))) (\lambda (t5:
578 T).(\lambda (_: T).(\lambda (t7: T).(ty3 g (CHead (CHead c0 (Bind b) t4)
579 (Bind b) u) t5 t7))))))) H17 u H11) in (let H22 \def (eq_ind T u0 (\lambda
580 (t4: T).(ty3 g (CHead c0 (Bind b) t4) t1 t2)) H18 u H11) in (let H23 \def
581 (eq_ind T u0 (\lambda (t4: T).((eq T t4 (THead (Bind b) u t1)) \to (ex4_3 T T
582 T (\lambda (t5: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u
583 t5) t)))) (\lambda (_: T).(\lambda (t6: T).(\lambda (_: T).(ty3 g c0 u t6))))
584 (\lambda (t5: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u)
585 t1 t5)))) (\lambda (t5: T).(\lambda (_: T).(\lambda (t7: T).(ty3 g (CHead c0
586 (Bind b) u) t5 t7))))))) H2 u H11) in (let H24 \def (eq_ind T u0 (\lambda
587 (t4: T).(ty3 g c0 t4 t)) H1 u H11) in (eq_ind_r T u (\lambda (t4: T).(ex4_3 T
588 T T (\lambda (t5: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind b)
589 u t5) (THead (Bind b) t4 t2))))) (\lambda (_: T).(\lambda (t6: T).(\lambda
590 (_: T).(ty3 g c0 u t6)))) (\lambda (t5: T).(\lambda (_: T).(\lambda (_:
591 T).(ty3 g (CHead c0 (Bind b) u) t1 t5)))) (\lambda (t5: T).(\lambda (_:
592 T).(\lambda (t7: T).(ty3 g (CHead c0 (Bind b) u) t5 t7)))))) (ex4_3_intro T T
593 T (\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u
594 t4) (THead (Bind b) u t2))))) (\lambda (_: T).(\lambda (t5: T).(\lambda (_:
595 T).(ty3 g c0 u t5)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(ty3 g
596 (CHead c0 (Bind b) u) t1 t4)))) (\lambda (t4: T).(\lambda (_: T).(\lambda
597 (t6: T).(ty3 g (CHead c0 (Bind b) u) t4 t6)))) t2 t t3 (pc3_refl c0 (THead
598 (Bind b) u t2)) H24 H22 H20) u0 H11))))))) b0 H12)))))))))) H9))
599 H8)))))))))))))))) (\lambda (c0: C).(\lambda (w: T).(\lambda (u0: T).(\lambda
600 (_: (ty3 g c0 w u0)).(\lambda (_: (((eq T w (THead (Bind b) u t1)) \to (ex4_3
601 T T T (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind
602 b) u t2) u0)))) (\lambda (_: T).(\lambda (t: T).(\lambda (_: T).(ty3 g c0 u
603 t)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind
604 b) u) t1 t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t0: T).(ty3 g
605 (CHead c0 (Bind b) u) t2 t0)))))))).(\lambda (v: T).(\lambda (t: T).(\lambda
606 (_: (ty3 g c0 v (THead (Bind Abst) u0 t))).(\lambda (_: (((eq T v (THead
607 (Bind b) u t1)) \to (ex4_3 T T T (\lambda (t2: T).(\lambda (_: T).(\lambda
608 (_: T).(pc3 c0 (THead (Bind b) u t2) (THead (Bind Abst) u0 t))))) (\lambda
609 (_: T).(\lambda (t0: T).(\lambda (_: T).(ty3 g c0 u t0)))) (\lambda (t2:
610 T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t2))))
611 (\lambda (t2: T).(\lambda (_: T).(\lambda (t3: T).(ty3 g (CHead c0 (Bind b)
612 u) t2 t3)))))))).(\lambda (H5: (eq T (THead (Flat Appl) w v) (THead (Bind b)
613 u t1))).(let H6 \def (eq_ind T (THead (Flat Appl) w v) (\lambda (ee:
614 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
615 False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K
616 return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _)
617 \Rightarrow True])])) I (THead (Bind b) u t1) H5) in (False_ind (ex4_3 T T T
618 (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u
619 t2) (THead (Flat Appl) w (THead (Bind Abst) u0 t)))))) (\lambda (_:
620 T).(\lambda (t0: T).(\lambda (_: T).(ty3 g c0 u t0)))) (\lambda (t2:
621 T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t2))))
622 (\lambda (t2: T).(\lambda (_: T).(\lambda (t3: T).(ty3 g (CHead c0 (Bind b)
623 u) t2 t3))))) H6)))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t2:
624 T).(\lambda (_: (ty3 g c0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind b) u
625 t1)) \to (ex4_3 T T T (\lambda (t3: T).(\lambda (_: T).(\lambda (_: T).(pc3
626 c0 (THead (Bind b) u t3) t2)))) (\lambda (_: T).(\lambda (t: T).(\lambda (_:
627 T).(ty3 g c0 u t)))) (\lambda (t3: T).(\lambda (_: T).(\lambda (_: T).(ty3 g
628 (CHead c0 (Bind b) u) t1 t3)))) (\lambda (t3: T).(\lambda (_: T).(\lambda
629 (t4: T).(ty3 g (CHead c0 (Bind b) u) t3 t4)))))))).(\lambda (t3: T).(\lambda
630 (_: (ty3 g c0 t2 t3)).(\lambda (_: (((eq T t2 (THead (Bind b) u t1)) \to
631 (ex4_3 T T T (\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead
632 (Bind b) u t4) t3)))) (\lambda (_: T).(\lambda (t: T).(\lambda (_: T).(ty3 g
633 c0 u t)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0
634 (Bind b) u) t1 t4)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (t5: T).(ty3
635 g (CHead c0 (Bind b) u) t4 t5)))))))).(\lambda (H5: (eq T (THead (Flat Cast)
636 t2 t0) (THead (Bind b) u t1))).(let H6 \def (eq_ind T (THead (Flat Cast) t2
637 t0) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
638 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
639 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
640 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) u t1)
641 H5) in (False_ind (ex4_3 T T T (\lambda (t4: T).(\lambda (_: T).(\lambda (_:
642 T).(pc3 c0 (THead (Bind b) u t4) (THead (Flat Cast) t3 t2))))) (\lambda (_:
643 T).(\lambda (t: T).(\lambda (_: T).(ty3 g c0 u t)))) (\lambda (t4:
644 T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t4))))
645 (\lambda (t4: T).(\lambda (_: T).(\lambda (t5: T).(ty3 g (CHead c0 (Bind b)
646 u) t4 t5))))) H6))))))))))) c y x H0))) H))))))).
648 theorem ty3_gen_appl:
649 \forall (g: G).(\forall (c: C).(\forall (w: T).(\forall (v: T).(\forall (x:
650 T).((ty3 g c (THead (Flat Appl) w v) x) \to (ex3_2 T T (\lambda (u:
651 T).(\lambda (t: T).(pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x)))
652 (\lambda (u: T).(\lambda (t: T).(ty3 g c v (THead (Bind Abst) u t))))
653 (\lambda (u: T).(\lambda (_: T).(ty3 g c w u)))))))))
655 \lambda (g: G).(\lambda (c: C).(\lambda (w: T).(\lambda (v: T).(\lambda (x:
656 T).(\lambda (H: (ty3 g c (THead (Flat Appl) w v) x)).(insert_eq T (THead
657 (Flat Appl) w v) (\lambda (t: T).(ty3 g c t x)) (ex3_2 T T (\lambda (u:
658 T).(\lambda (t: T).(pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x)))
659 (\lambda (u: T).(\lambda (t: T).(ty3 g c v (THead (Bind Abst) u t))))
660 (\lambda (u: T).(\lambda (_: T).(ty3 g c w u)))) (\lambda (y: T).(\lambda
661 (H0: (ty3 g c y x)).(ty3_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0:
662 T).((eq T t (THead (Flat Appl) w v)) \to (ex3_2 T T (\lambda (u: T).(\lambda
663 (t1: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u t1)) t0))) (\lambda
664 (u: T).(\lambda (t1: T).(ty3 g c0 v (THead (Bind Abst) u t1)))) (\lambda (u:
665 T).(\lambda (_: T).(ty3 g c0 w u)))))))) (\lambda (c0: C).(\lambda (t2:
666 T).(\lambda (t: T).(\lambda (_: (ty3 g c0 t2 t)).(\lambda (_: (((eq T t2
667 (THead (Flat Appl) w v)) \to (ex3_2 T T (\lambda (u: T).(\lambda (t0: T).(pc3
668 c0 (THead (Flat Appl) w (THead (Bind Abst) u t0)) t))) (\lambda (u:
669 T).(\lambda (t0: T).(ty3 g c0 v (THead (Bind Abst) u t0)))) (\lambda (u:
670 T).(\lambda (_: T).(ty3 g c0 w u))))))).(\lambda (u: T).(\lambda (t1:
671 T).(\lambda (H3: (ty3 g c0 u t1)).(\lambda (H4: (((eq T u (THead (Flat Appl)
672 w v)) \to (ex3_2 T T (\lambda (u0: T).(\lambda (t0: T).(pc3 c0 (THead (Flat
673 Appl) w (THead (Bind Abst) u0 t0)) t1))) (\lambda (u0: T).(\lambda (t0:
674 T).(ty3 g c0 v (THead (Bind Abst) u0 t0)))) (\lambda (u0: T).(\lambda (_:
675 T).(ty3 g c0 w u0))))))).(\lambda (H5: (pc3 c0 t1 t2)).(\lambda (H6: (eq T u
676 (THead (Flat Appl) w v))).(let H7 \def (f_equal T T (\lambda (e: T).e) u
677 (THead (Flat Appl) w v) H6) in (let H8 \def (eq_ind T u (\lambda (t0: T).((eq
678 T t0 (THead (Flat Appl) w v)) \to (ex3_2 T T (\lambda (u0: T).(\lambda (t3:
679 T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t3)) t1))) (\lambda
680 (u0: T).(\lambda (t3: T).(ty3 g c0 v (THead (Bind Abst) u0 t3)))) (\lambda
681 (u0: T).(\lambda (_: T).(ty3 g c0 w u0)))))) H4 (THead (Flat Appl) w v) H7)
682 in (let H9 \def (eq_ind T u (\lambda (t0: T).(ty3 g c0 t0 t1)) H3 (THead
683 (Flat Appl) w v) H7) in (let H10 \def (H8 (refl_equal T (THead (Flat Appl) w
684 v))) in (ex3_2_ind T T (\lambda (u0: T).(\lambda (t0: T).(pc3 c0 (THead (Flat
685 Appl) w (THead (Bind Abst) u0 t0)) t1))) (\lambda (u0: T).(\lambda (t0:
686 T).(ty3 g c0 v (THead (Bind Abst) u0 t0)))) (\lambda (u0: T).(\lambda (_:
687 T).(ty3 g c0 w u0))) (ex3_2 T T (\lambda (u0: T).(\lambda (t0: T).(pc3 c0
688 (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t2))) (\lambda (u0:
689 T).(\lambda (t0: T).(ty3 g c0 v (THead (Bind Abst) u0 t0)))) (\lambda (u0:
690 T).(\lambda (_: T).(ty3 g c0 w u0)))) (\lambda (x0: T).(\lambda (x1:
691 T).(\lambda (H11: (pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) x0 x1))
692 t1)).(\lambda (H12: (ty3 g c0 v (THead (Bind Abst) x0 x1))).(\lambda (H13:
693 (ty3 g c0 w x0)).(ex3_2_intro T T (\lambda (u0: T).(\lambda (t0: T).(pc3 c0
694 (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t2))) (\lambda (u0:
695 T).(\lambda (t0: T).(ty3 g c0 v (THead (Bind Abst) u0 t0)))) (\lambda (u0:
696 T).(\lambda (_: T).(ty3 g c0 w u0))) x0 x1 (pc3_t t1 c0 (THead (Flat Appl) w
697 (THead (Bind Abst) x0 x1)) H11 t2 H5) H12 H13)))))) H10))))))))))))))))
698 (\lambda (c0: C).(\lambda (m: nat).(\lambda (H1: (eq T (TSort m) (THead (Flat
699 Appl) w v))).(let H2 \def (eq_ind T (TSort m) (\lambda (ee: T).(match ee in T
700 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _)
701 \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) w
702 v) H1) in (False_ind (ex3_2 T T (\lambda (u: T).(\lambda (t: T).(pc3 c0
703 (THead (Flat Appl) w (THead (Bind Abst) u t)) (TSort (next g m))))) (\lambda
704 (u: T).(\lambda (t: T).(ty3 g c0 v (THead (Bind Abst) u t)))) (\lambda (u:
705 T).(\lambda (_: T).(ty3 g c0 w u)))) H2))))) (\lambda (n: nat).(\lambda (c0:
706 C).(\lambda (d: C).(\lambda (u: T).(\lambda (_: (getl n c0 (CHead d (Bind
707 Abbr) u))).(\lambda (t: T).(\lambda (_: (ty3 g d u t)).(\lambda (_: (((eq T u
708 (THead (Flat Appl) w v)) \to (ex3_2 T T (\lambda (u0: T).(\lambda (t0:
709 T).(pc3 d (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t))) (\lambda (u0:
710 T).(\lambda (t0: T).(ty3 g d v (THead (Bind Abst) u0 t0)))) (\lambda (u0:
711 T).(\lambda (_: T).(ty3 g d w u0))))))).(\lambda (H4: (eq T (TLRef n) (THead
712 (Flat Appl) w v))).(let H5 \def (eq_ind T (TLRef n) (\lambda (ee: T).(match
713 ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False |
714 (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead
715 (Flat Appl) w v) H4) in (False_ind (ex3_2 T T (\lambda (u0: T).(\lambda (t0:
716 T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) (lift (S n) O
717 t)))) (\lambda (u0: T).(\lambda (t0: T).(ty3 g c0 v (THead (Bind Abst) u0
718 t0)))) (\lambda (u0: T).(\lambda (_: T).(ty3 g c0 w u0)))) H5)))))))))))
719 (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda
720 (_: (getl n c0 (CHead d (Bind Abst) u))).(\lambda (t: T).(\lambda (_: (ty3 g
721 d u t)).(\lambda (_: (((eq T u (THead (Flat Appl) w v)) \to (ex3_2 T T
722 (\lambda (u0: T).(\lambda (t0: T).(pc3 d (THead (Flat Appl) w (THead (Bind
723 Abst) u0 t0)) t))) (\lambda (u0: T).(\lambda (t0: T).(ty3 g d v (THead (Bind
724 Abst) u0 t0)))) (\lambda (u0: T).(\lambda (_: T).(ty3 g d w
725 u0))))))).(\lambda (H4: (eq T (TLRef n) (THead (Flat Appl) w v))).(let H5
726 \def (eq_ind T (TLRef n) (\lambda (ee: T).(match ee in T return (\lambda (_:
727 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
728 (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) w v) H4) in
729 (False_ind (ex3_2 T T (\lambda (u0: T).(\lambda (t0: T).(pc3 c0 (THead (Flat
730 Appl) w (THead (Bind Abst) u0 t0)) (lift (S n) O u)))) (\lambda (u0:
731 T).(\lambda (t0: T).(ty3 g c0 v (THead (Bind Abst) u0 t0)))) (\lambda (u0:
732 T).(\lambda (_: T).(ty3 g c0 w u0)))) H5))))))))))) (\lambda (c0: C).(\lambda
733 (u: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 u t)).(\lambda (_: (((eq T u
734 (THead (Flat Appl) w v)) \to (ex3_2 T T (\lambda (u0: T).(\lambda (t0:
735 T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t0)) t))) (\lambda (u0:
736 T).(\lambda (t0: T).(ty3 g c0 v (THead (Bind Abst) u0 t0)))) (\lambda (u0:
737 T).(\lambda (_: T).(ty3 g c0 w u0))))))).(\lambda (b: B).(\lambda (t1:
738 T).(\lambda (t2: T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t1
739 t2)).(\lambda (_: (((eq T t1 (THead (Flat Appl) w v)) \to (ex3_2 T T (\lambda
740 (u0: T).(\lambda (t0: T).(pc3 (CHead c0 (Bind b) u) (THead (Flat Appl) w
741 (THead (Bind Abst) u0 t0)) t2))) (\lambda (u0: T).(\lambda (t0: T).(ty3 g
742 (CHead c0 (Bind b) u) v (THead (Bind Abst) u0 t0)))) (\lambda (u0:
743 T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) w u0))))))).(\lambda (t0:
744 T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t2 t0)).(\lambda (_: (((eq T t2
745 (THead (Flat Appl) w v)) \to (ex3_2 T T (\lambda (u0: T).(\lambda (t3:
746 T).(pc3 (CHead c0 (Bind b) u) (THead (Flat Appl) w (THead (Bind Abst) u0 t3))
747 t0))) (\lambda (u0: T).(\lambda (t3: T).(ty3 g (CHead c0 (Bind b) u) v (THead
748 (Bind Abst) u0 t3)))) (\lambda (u0: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind
749 b) u) w u0))))))).(\lambda (H7: (eq T (THead (Bind b) u t1) (THead (Flat
750 Appl) w v))).(let H8 \def (eq_ind T (THead (Bind b) u t1) (\lambda (ee:
751 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
752 False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K
753 return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _)
754 \Rightarrow False])])) I (THead (Flat Appl) w v) H7) in (False_ind (ex3_2 T T
755 (\lambda (u0: T).(\lambda (t3: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind
756 Abst) u0 t3)) (THead (Bind b) u t2)))) (\lambda (u0: T).(\lambda (t3: T).(ty3
757 g c0 v (THead (Bind Abst) u0 t3)))) (\lambda (u0: T).(\lambda (_: T).(ty3 g
758 c0 w u0)))) H8)))))))))))))))) (\lambda (c0: C).(\lambda (w0: T).(\lambda (u:
759 T).(\lambda (H1: (ty3 g c0 w0 u)).(\lambda (H2: (((eq T w0 (THead (Flat Appl)
760 w v)) \to (ex3_2 T T (\lambda (u0: T).(\lambda (t: T).(pc3 c0 (THead (Flat
761 Appl) w (THead (Bind Abst) u0 t)) u))) (\lambda (u0: T).(\lambda (t: T).(ty3
762 g c0 v (THead (Bind Abst) u0 t)))) (\lambda (u0: T).(\lambda (_: T).(ty3 g c0
763 w u0))))))).(\lambda (v0: T).(\lambda (t: T).(\lambda (H3: (ty3 g c0 v0
764 (THead (Bind Abst) u t))).(\lambda (H4: (((eq T v0 (THead (Flat Appl) w v))
765 \to (ex3_2 T T (\lambda (u0: T).(\lambda (t0: T).(pc3 c0 (THead (Flat Appl) w
766 (THead (Bind Abst) u0 t0)) (THead (Bind Abst) u t)))) (\lambda (u0:
767 T).(\lambda (t0: T).(ty3 g c0 v (THead (Bind Abst) u0 t0)))) (\lambda (u0:
768 T).(\lambda (_: T).(ty3 g c0 w u0))))))).(\lambda (H5: (eq T (THead (Flat
769 Appl) w0 v0) (THead (Flat Appl) w v))).(let H6 \def (f_equal T T (\lambda (e:
770 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow w0 |
771 (TLRef _) \Rightarrow w0 | (THead _ t0 _) \Rightarrow t0])) (THead (Flat
772 Appl) w0 v0) (THead (Flat Appl) w v) H5) in ((let H7 \def (f_equal T T
773 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
774 \Rightarrow v0 | (TLRef _) \Rightarrow v0 | (THead _ _ t0) \Rightarrow t0]))
775 (THead (Flat Appl) w0 v0) (THead (Flat Appl) w v) H5) in (\lambda (H8: (eq T
776 w0 w)).(let H9 \def (eq_ind T v0 (\lambda (t0: T).((eq T t0 (THead (Flat
777 Appl) w v)) \to (ex3_2 T T (\lambda (u0: T).(\lambda (t1: T).(pc3 c0 (THead
778 (Flat Appl) w (THead (Bind Abst) u0 t1)) (THead (Bind Abst) u t)))) (\lambda
779 (u0: T).(\lambda (t1: T).(ty3 g c0 v (THead (Bind Abst) u0 t1)))) (\lambda
780 (u0: T).(\lambda (_: T).(ty3 g c0 w u0)))))) H4 v H7) in (let H10 \def
781 (eq_ind T v0 (\lambda (t0: T).(ty3 g c0 t0 (THead (Bind Abst) u t))) H3 v H7)
782 in (let H11 \def (eq_ind T w0 (\lambda (t0: T).((eq T t0 (THead (Flat Appl) w
783 v)) \to (ex3_2 T T (\lambda (u0: T).(\lambda (t1: T).(pc3 c0 (THead (Flat
784 Appl) w (THead (Bind Abst) u0 t1)) u))) (\lambda (u0: T).(\lambda (t1:
785 T).(ty3 g c0 v (THead (Bind Abst) u0 t1)))) (\lambda (u0: T).(\lambda (_:
786 T).(ty3 g c0 w u0)))))) H2 w H8) in (let H12 \def (eq_ind T w0 (\lambda (t0:
787 T).(ty3 g c0 t0 u)) H1 w H8) in (eq_ind_r T w (\lambda (t0: T).(ex3_2 T T
788 (\lambda (u0: T).(\lambda (t1: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind
789 Abst) u0 t1)) (THead (Flat Appl) t0 (THead (Bind Abst) u t))))) (\lambda (u0:
790 T).(\lambda (t1: T).(ty3 g c0 v (THead (Bind Abst) u0 t1)))) (\lambda (u0:
791 T).(\lambda (_: T).(ty3 g c0 w u0))))) (ex3_2_intro T T (\lambda (u0:
792 T).(\lambda (t0: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t0))
793 (THead (Flat Appl) w (THead (Bind Abst) u t))))) (\lambda (u0: T).(\lambda
794 (t0: T).(ty3 g c0 v (THead (Bind Abst) u0 t0)))) (\lambda (u0: T).(\lambda
795 (_: T).(ty3 g c0 w u0))) u t (pc3_refl c0 (THead (Flat Appl) w (THead (Bind
796 Abst) u t))) H10 H12) w0 H8))))))) H6)))))))))))) (\lambda (c0: C).(\lambda
797 (t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g c0 t1 t2)).(\lambda (_: (((eq T
798 t1 (THead (Flat Appl) w v)) \to (ex3_2 T T (\lambda (u: T).(\lambda (t:
799 T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t2))) (\lambda (u:
800 T).(\lambda (t: T).(ty3 g c0 v (THead (Bind Abst) u t)))) (\lambda (u:
801 T).(\lambda (_: T).(ty3 g c0 w u))))))).(\lambda (t0: T).(\lambda (_: (ty3 g
802 c0 t2 t0)).(\lambda (_: (((eq T t2 (THead (Flat Appl) w v)) \to (ex3_2 T T
803 (\lambda (u: T).(\lambda (t: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind
804 Abst) u t)) t0))) (\lambda (u: T).(\lambda (t: T).(ty3 g c0 v (THead (Bind
805 Abst) u t)))) (\lambda (u: T).(\lambda (_: T).(ty3 g c0 w u))))))).(\lambda
806 (H5: (eq T (THead (Flat Cast) t2 t1) (THead (Flat Appl) w v))).(let H6 \def
807 (eq_ind T (THead (Flat Cast) t2 t1) (\lambda (ee: T).(match ee in T return
808 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
809 \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda
810 (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat f) \Rightarrow (match f
811 in F return (\lambda (_: F).Prop) with [Appl \Rightarrow False | Cast
812 \Rightarrow True])])])) I (THead (Flat Appl) w v) H5) in (False_ind (ex3_2 T
813 T (\lambda (u: T).(\lambda (t: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind
814 Abst) u t)) (THead (Flat Cast) t0 t2)))) (\lambda (u: T).(\lambda (t: T).(ty3
815 g c0 v (THead (Bind Abst) u t)))) (\lambda (u: T).(\lambda (_: T).(ty3 g c0 w
816 u)))) H6))))))))))) c y x H0))) H)))))).
818 theorem ty3_gen_cast:
819 \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).(\forall
820 (x: T).((ty3 g c (THead (Flat Cast) t2 t1) x) \to (ex3 T (\lambda (t0:
821 T).(pc3 c (THead (Flat Cast) t0 t2) x)) (\lambda (_: T).(ty3 g c t1 t2))
822 (\lambda (t0: T).(ty3 g c t2 t0))))))))
824 \lambda (g: G).(\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
825 (x: T).(\lambda (H: (ty3 g c (THead (Flat Cast) t2 t1) x)).(insert_eq T
826 (THead (Flat Cast) t2 t1) (\lambda (t: T).(ty3 g c t x)) (ex3 T (\lambda (t0:
827 T).(pc3 c (THead (Flat Cast) t0 t2) x)) (\lambda (_: T).(ty3 g c t1 t2))
828 (\lambda (t0: T).(ty3 g c t2 t0))) (\lambda (y: T).(\lambda (H0: (ty3 g c y
829 x)).(ty3_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).((eq T t
830 (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t3: T).(pc3 c0 (THead (Flat
831 Cast) t3 t2) t0)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t3: T).(ty3 g
832 c0 t2 t3))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t: T).(\lambda
833 (_: (ty3 g c0 t0 t)).(\lambda (_: (((eq T t0 (THead (Flat Cast) t2 t1)) \to
834 (ex3 T (\lambda (t3: T).(pc3 c0 (THead (Flat Cast) t3 t2) t)) (\lambda (_:
835 T).(ty3 g c0 t1 t2)) (\lambda (t3: T).(ty3 g c0 t2 t3)))))).(\lambda (u:
836 T).(\lambda (t3: T).(\lambda (H3: (ty3 g c0 u t3)).(\lambda (H4: (((eq T u
837 (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t4: T).(pc3 c0 (THead (Flat
838 Cast) t4 t2) t3)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t4: T).(ty3 g
839 c0 t2 t4)))))).(\lambda (H5: (pc3 c0 t3 t0)).(\lambda (H6: (eq T u (THead
840 (Flat Cast) t2 t1))).(let H7 \def (f_equal T T (\lambda (e: T).e) u (THead
841 (Flat Cast) t2 t1) H6) in (let H8 \def (eq_ind T u (\lambda (t4: T).((eq T t4
842 (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t5: T).(pc3 c0 (THead (Flat
843 Cast) t5 t2) t3)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g
844 c0 t2 t5))))) H4 (THead (Flat Cast) t2 t1) H7) in (let H9 \def (eq_ind T u
845 (\lambda (t4: T).(ty3 g c0 t4 t3)) H3 (THead (Flat Cast) t2 t1) H7) in (let
846 H10 \def (H8 (refl_equal T (THead (Flat Cast) t2 t1))) in (ex3_ind T (\lambda
847 (t4: T).(pc3 c0 (THead (Flat Cast) t4 t2) t3)) (\lambda (_: T).(ty3 g c0 t1
848 t2)) (\lambda (t4: T).(ty3 g c0 t2 t4)) (ex3 T (\lambda (t4: T).(pc3 c0
849 (THead (Flat Cast) t4 t2) t0)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda
850 (t4: T).(ty3 g c0 t2 t4))) (\lambda (x0: T).(\lambda (H11: (pc3 c0 (THead
851 (Flat Cast) x0 t2) t3)).(\lambda (H12: (ty3 g c0 t1 t2)).(\lambda (H13: (ty3
852 g c0 t2 x0)).(ex3_intro T (\lambda (t4: T).(pc3 c0 (THead (Flat Cast) t4 t2)
853 t0)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t4: T).(ty3 g c0 t2 t4)) x0
854 (pc3_t t3 c0 (THead (Flat Cast) x0 t2) H11 t0 H5) H12 H13)))))
855 H10)))))))))))))))) (\lambda (c0: C).(\lambda (m: nat).(\lambda (H1: (eq T
856 (TSort m) (THead (Flat Cast) t2 t1))).(let H2 \def (eq_ind T (TSort m)
857 (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
858 \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
859 False])) I (THead (Flat Cast) t2 t1) H1) in (False_ind (ex3 T (\lambda (t0:
860 T).(pc3 c0 (THead (Flat Cast) t0 t2) (TSort (next g m)))) (\lambda (_:
861 T).(ty3 g c0 t1 t2)) (\lambda (t0: T).(ty3 g c0 t2 t0))) H2))))) (\lambda (n:
862 nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (_: (getl n c0
863 (CHead d (Bind Abbr) u))).(\lambda (t: T).(\lambda (_: (ty3 g d u
864 t)).(\lambda (_: (((eq T u (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda
865 (t0: T).(pc3 d (THead (Flat Cast) t0 t2) t)) (\lambda (_: T).(ty3 g d t1 t2))
866 (\lambda (t0: T).(ty3 g d t2 t0)))))).(\lambda (H4: (eq T (TLRef n) (THead
867 (Flat Cast) t2 t1))).(let H5 \def (eq_ind T (TLRef n) (\lambda (ee: T).(match
868 ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False |
869 (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead
870 (Flat Cast) t2 t1) H4) in (False_ind (ex3 T (\lambda (t0: T).(pc3 c0 (THead
871 (Flat Cast) t0 t2) (lift (S n) O t))) (\lambda (_: T).(ty3 g c0 t1 t2))
872 (\lambda (t0: T).(ty3 g c0 t2 t0))) H5))))))))))) (\lambda (n: nat).(\lambda
873 (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (_: (getl n c0 (CHead d
874 (Bind Abst) u))).(\lambda (t: T).(\lambda (_: (ty3 g d u t)).(\lambda (_:
875 (((eq T u (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t0: T).(pc3 d
876 (THead (Flat Cast) t0 t2) t)) (\lambda (_: T).(ty3 g d t1 t2)) (\lambda (t0:
877 T).(ty3 g d t2 t0)))))).(\lambda (H4: (eq T (TLRef n) (THead (Flat Cast) t2
878 t1))).(let H5 \def (eq_ind T (TLRef n) (\lambda (ee: T).(match ee in T return
879 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
880 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Flat Cast) t2
881 t1) H4) in (False_ind (ex3 T (\lambda (t0: T).(pc3 c0 (THead (Flat Cast) t0
882 t2) (lift (S n) O u))) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t0:
883 T).(ty3 g c0 t2 t0))) H5))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda
884 (t: T).(\lambda (_: (ty3 g c0 u t)).(\lambda (_: (((eq T u (THead (Flat Cast)
885 t2 t1)) \to (ex3 T (\lambda (t0: T).(pc3 c0 (THead (Flat Cast) t0 t2) t))
886 (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t0: T).(ty3 g c0 t2
887 t0)))))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3
888 g (CHead c0 (Bind b) u) t0 t3)).(\lambda (_: (((eq T t0 (THead (Flat Cast) t2
889 t1)) \to (ex3 T (\lambda (t4: T).(pc3 (CHead c0 (Bind b) u) (THead (Flat
890 Cast) t4 t2) t3)) (\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t2))
891 (\lambda (t4: T).(ty3 g (CHead c0 (Bind b) u) t2 t4)))))).(\lambda (t4:
892 T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t3 t4)).(\lambda (_: (((eq T t3
893 (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t5: T).(pc3 (CHead c0 (Bind
894 b) u) (THead (Flat Cast) t5 t2) t4)) (\lambda (_: T).(ty3 g (CHead c0 (Bind
895 b) u) t1 t2)) (\lambda (t5: T).(ty3 g (CHead c0 (Bind b) u) t2
896 t5)))))).(\lambda (H7: (eq T (THead (Bind b) u t0) (THead (Flat Cast) t2
897 t1))).(let H8 \def (eq_ind T (THead (Bind b) u t0) (\lambda (ee: T).(match ee
898 in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef
899 _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return
900 (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow
901 False])])) I (THead (Flat Cast) t2 t1) H7) in (False_ind (ex3 T (\lambda (t5:
902 T).(pc3 c0 (THead (Flat Cast) t5 t2) (THead (Bind b) u t3))) (\lambda (_:
903 T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5))) H8))))))))))))))))
904 (\lambda (c0: C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 g c0 w
905 u)).(\lambda (_: (((eq T w (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda
906 (t0: T).(pc3 c0 (THead (Flat Cast) t0 t2) u)) (\lambda (_: T).(ty3 g c0 t1
907 t2)) (\lambda (t0: T).(ty3 g c0 t2 t0)))))).(\lambda (v: T).(\lambda (t:
908 T).(\lambda (_: (ty3 g c0 v (THead (Bind Abst) u t))).(\lambda (_: (((eq T v
909 (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t0: T).(pc3 c0 (THead (Flat
910 Cast) t0 t2) (THead (Bind Abst) u t))) (\lambda (_: T).(ty3 g c0 t1 t2))
911 (\lambda (t0: T).(ty3 g c0 t2 t0)))))).(\lambda (H5: (eq T (THead (Flat Appl)
912 w v) (THead (Flat Cast) t2 t1))).(let H6 \def (eq_ind T (THead (Flat Appl) w
913 v) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
914 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
915 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
916 \Rightarrow False | (Flat f) \Rightarrow (match f in F return (\lambda (_:
917 F).Prop) with [Appl \Rightarrow True | Cast \Rightarrow False])])])) I (THead
918 (Flat Cast) t2 t1) H5) in (False_ind (ex3 T (\lambda (t0: T).(pc3 c0 (THead
919 (Flat Cast) t0 t2) (THead (Flat Appl) w (THead (Bind Abst) u t)))) (\lambda
920 (_: T).(ty3 g c0 t1 t2)) (\lambda (t0: T).(ty3 g c0 t2 t0))) H6))))))))))))
921 (\lambda (c0: C).(\lambda (t0: T).(\lambda (t3: T).(\lambda (H1: (ty3 g c0 t0
922 t3)).(\lambda (H2: (((eq T t0 (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda
923 (t4: T).(pc3 c0 (THead (Flat Cast) t4 t2) t3)) (\lambda (_: T).(ty3 g c0 t1
924 t2)) (\lambda (t4: T).(ty3 g c0 t2 t4)))))).(\lambda (t4: T).(\lambda (H3:
925 (ty3 g c0 t3 t4)).(\lambda (H4: (((eq T t3 (THead (Flat Cast) t2 t1)) \to
926 (ex3 T (\lambda (t5: T).(pc3 c0 (THead (Flat Cast) t5 t2) t4)) (\lambda (_:
927 T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5)))))).(\lambda (H5: (eq
928 T (THead (Flat Cast) t3 t0) (THead (Flat Cast) t2 t1))).(let H6 \def (f_equal
929 T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
930 \Rightarrow t3 | (TLRef _) \Rightarrow t3 | (THead _ t _) \Rightarrow t]))
931 (THead (Flat Cast) t3 t0) (THead (Flat Cast) t2 t1) H5) in ((let H7 \def
932 (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with
933 [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t)
934 \Rightarrow t])) (THead (Flat Cast) t3 t0) (THead (Flat Cast) t2 t1) H5) in
935 (\lambda (H8: (eq T t3 t2)).(let H9 \def (eq_ind T t3 (\lambda (t: T).((eq T
936 t (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t5: T).(pc3 c0 (THead (Flat
937 Cast) t5 t2) t4)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g
938 c0 t2 t5))))) H4 t2 H8) in (let H10 \def (eq_ind T t3 (\lambda (t: T).(ty3 g
939 c0 t t4)) H3 t2 H8) in (let H11 \def (eq_ind T t3 (\lambda (t: T).((eq T t0
940 (THead (Flat Cast) t2 t1)) \to (ex3 T (\lambda (t5: T).(pc3 c0 (THead (Flat
941 Cast) t5 t2) t)) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g c0
942 t2 t5))))) H2 t2 H8) in (let H12 \def (eq_ind T t3 (\lambda (t: T).(ty3 g c0
943 t0 t)) H1 t2 H8) in (eq_ind_r T t2 (\lambda (t: T).(ex3 T (\lambda (t5:
944 T).(pc3 c0 (THead (Flat Cast) t5 t2) (THead (Flat Cast) t4 t))) (\lambda (_:
945 T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5)))) (let H13 \def
946 (eq_ind T t0 (\lambda (t: T).((eq T t (THead (Flat Cast) t2 t1)) \to (ex3 T
947 (\lambda (t5: T).(pc3 c0 (THead (Flat Cast) t5 t2) t2)) (\lambda (_: T).(ty3
948 g c0 t1 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5))))) H11 t1 H7) in (let H14
949 \def (eq_ind T t0 (\lambda (t: T).(ty3 g c0 t t2)) H12 t1 H7) in (ex3_intro T
950 (\lambda (t5: T).(pc3 c0 (THead (Flat Cast) t5 t2) (THead (Flat Cast) t4
951 t2))) (\lambda (_: T).(ty3 g c0 t1 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5)) t4
952 (pc3_refl c0 (THead (Flat Cast) t4 t2)) H14 H10))) t3 H8))))))) H6)))))))))))
projects / helm.git / blob