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