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/Level-1/LambdaDelta/ty3/dec".
19 include "ty3/pr3_props.ma".
23 include "getl/flt.ma".
25 include "getl/dec.ma".
27 theorem ty3_inference:
28 \forall (g: G).(\forall (c: C).(\forall (t1: T).(or (ex T (\lambda (t2:
29 T).(ty3 g c t1 t2))) (\forall (t2: T).((ty3 g c t1 t2) \to (\forall (P:
32 \lambda (g: G).(\lambda (c: C).(\lambda (t1: T).(flt_wf_ind (\lambda (c0:
33 C).(\lambda (t: T).(or (ex T (\lambda (t2: T).(ty3 g c0 t t2))) (\forall (t2:
34 T).((ty3 g c0 t t2) \to (\forall (P: Prop).P)))))) (\lambda (c2: C).(\lambda
35 (t2: T).(T_ind (\lambda (t: T).(((\forall (c1: C).(\forall (t3: T).((flt c1
36 t3 c2 t) \to (or (ex T (\lambda (t4: T).(ty3 g c1 t3 t4))) (\forall (t4:
37 T).((ty3 g c1 t3 t4) \to (\forall (P: Prop).P)))))))) \to (or (ex T (\lambda
38 (t3: T).(ty3 g c2 t t3))) (\forall (t3: T).((ty3 g c2 t t3) \to (\forall (P:
39 Prop).P)))))) (\lambda (n: nat).(\lambda (_: ((\forall (c1: C).(\forall (t3:
40 T).((flt c1 t3 c2 (TSort n)) \to (or (ex T (\lambda (t4: T).(ty3 g c1 t3
41 t4))) (\forall (t4: T).((ty3 g c1 t3 t4) \to (\forall (P:
42 Prop).P))))))))).(or_introl (ex T (\lambda (t3: T).(ty3 g c2 (TSort n) t3)))
43 (\forall (t3: T).((ty3 g c2 (TSort n) t3) \to (\forall (P: Prop).P)))
44 (ex_intro T (\lambda (t3: T).(ty3 g c2 (TSort n) t3)) (TSort (next g n))
45 (ty3_sort g c2 n))))) (\lambda (n: nat).(\lambda (H: ((\forall (c1:
46 C).(\forall (t3: T).((flt c1 t3 c2 (TLRef n)) \to (or (ex T (\lambda (t4:
47 T).(ty3 g c1 t3 t4))) (\forall (t4: T).((ty3 g c1 t3 t4) \to (\forall (P:
48 Prop).P))))))))).(let H_x \def (getl_dec c2 n) in (let H0 \def H_x in (or_ind
49 (ex_3 C B T (\lambda (e: C).(\lambda (b: B).(\lambda (v: T).(getl n c2 (CHead
50 e (Bind b) v)))))) (\forall (d: C).((getl n c2 d) \to (\forall (P: Prop).P)))
51 (or (ex T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3))) (\forall (t3: T).((ty3 g
52 c2 (TLRef n) t3) \to (\forall (P: Prop).P)))) (\lambda (H1: (ex_3 C B T
53 (\lambda (e: C).(\lambda (b: B).(\lambda (v: T).(getl n c2 (CHead e (Bind b)
54 v))))))).(ex_3_ind C B T (\lambda (e: C).(\lambda (b: B).(\lambda (v:
55 T).(getl n c2 (CHead e (Bind b) v))))) (or (ex T (\lambda (t3: T).(ty3 g c2
56 (TLRef n) t3))) (\forall (t3: T).((ty3 g c2 (TLRef n) t3) \to (\forall (P:
57 Prop).P)))) (\lambda (x0: C).(\lambda (x1: B).(\lambda (x2: T).(\lambda (H2:
58 (getl n c2 (CHead x0 (Bind x1) x2))).(let H3 \def (H x0 x2 (getl_flt x1 c2 x0
59 x2 n H2)) in (or_ind (ex T (\lambda (t3: T).(ty3 g x0 x2 t3))) (\forall (t3:
60 T).((ty3 g x0 x2 t3) \to (\forall (P: Prop).P))) (or (ex T (\lambda (t3:
61 T).(ty3 g c2 (TLRef n) t3))) (\forall (t3: T).((ty3 g c2 (TLRef n) t3) \to
62 (\forall (P: Prop).P)))) (\lambda (H4: (ex T (\lambda (t3: T).(ty3 g x0 x2
63 t3)))).(ex_ind T (\lambda (t3: T).(ty3 g x0 x2 t3)) (or (ex T (\lambda (t3:
64 T).(ty3 g c2 (TLRef n) t3))) (\forall (t3: T).((ty3 g c2 (TLRef n) t3) \to
65 (\forall (P: Prop).P)))) (\lambda (x: T).(\lambda (H5: (ty3 g x0 x2
66 x)).(B_ind (\lambda (b: B).((getl n c2 (CHead x0 (Bind b) x2)) \to (or (ex T
67 (\lambda (t3: T).(ty3 g c2 (TLRef n) t3))) (\forall (t3: T).((ty3 g c2 (TLRef
68 n) t3) \to (\forall (P: Prop).P)))))) (\lambda (H6: (getl n c2 (CHead x0
69 (Bind Abbr) x2))).(or_introl (ex T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3)))
70 (\forall (t3: T).((ty3 g c2 (TLRef n) t3) \to (\forall (P: Prop).P)))
71 (ex_intro T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3)) (lift (S n) O x)
72 (ty3_abbr g n c2 x0 x2 H6 x H5)))) (\lambda (H6: (getl n c2 (CHead x0 (Bind
73 Abst) x2))).(or_introl (ex T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3)))
74 (\forall (t3: T).((ty3 g c2 (TLRef n) t3) \to (\forall (P: Prop).P)))
75 (ex_intro T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3)) (lift (S n) O x2)
76 (ty3_abst g n c2 x0 x2 H6 x H5)))) (\lambda (H6: (getl n c2 (CHead x0 (Bind
77 Void) x2))).(or_intror (ex T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3)))
78 (\forall (t3: T).((ty3 g c2 (TLRef n) t3) \to (\forall (P: Prop).P)))
79 (\lambda (t3: T).(\lambda (H7: (ty3 g c2 (TLRef n) t3)).(\lambda (P:
80 Prop).(or_ind (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t:
81 T).(pc3 c2 (lift (S n) O t) t3)))) (\lambda (e: C).(\lambda (u: T).(\lambda
82 (_: T).(getl n c2 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
83 T).(\lambda (t: T).(ty3 g e u t))))) (ex3_3 C T T (\lambda (_: C).(\lambda
84 (u: T).(\lambda (_: T).(pc3 c2 (lift (S n) O u) t3)))) (\lambda (e:
85 C).(\lambda (u: T).(\lambda (_: T).(getl n c2 (CHead e (Bind Abst) u)))))
86 (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t))))) P (\lambda
87 (H8: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 c2
88 (lift (S n) O t) t3)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl
89 n c2 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t:
90 T).(ty3 g e u t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_:
91 T).(\lambda (t: T).(pc3 c2 (lift (S n) O t) t3)))) (\lambda (e: C).(\lambda
92 (u: T).(\lambda (_: T).(getl n c2 (CHead e (Bind Abbr) u))))) (\lambda (e:
93 C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t)))) P (\lambda (x3:
94 C).(\lambda (x4: T).(\lambda (x5: T).(\lambda (_: (pc3 c2 (lift (S n) O x5)
95 t3)).(\lambda (H10: (getl n c2 (CHead x3 (Bind Abbr) x4))).(\lambda (_: (ty3
96 g x3 x4 x5)).(let H12 \def (eq_ind C (CHead x0 (Bind Void) x2) (\lambda (c0:
97 C).(getl n c2 c0)) H6 (CHead x3 (Bind Abbr) x4) (getl_mono c2 (CHead x0 (Bind
98 Void) x2) n H6 (CHead x3 (Bind Abbr) x4) H10)) in (let H13 \def (eq_ind C
99 (CHead x0 (Bind Void) x2) (\lambda (ee: C).(match ee in C return (\lambda (_:
100 C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
101 k in K return (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B
102 return (\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow
103 False | Void \Rightarrow True]) | (Flat _) \Rightarrow False])])) I (CHead x3
104 (Bind Abbr) x4) (getl_mono c2 (CHead x0 (Bind Void) x2) n H6 (CHead x3 (Bind
105 Abbr) x4) H10)) in (False_ind P H13))))))))) H8)) (\lambda (H8: (ex3_3 C T T
106 (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(pc3 c2 (lift (S n) O u)
107 t3)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c2 (CHead e
108 (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u
109 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(pc3
110 c2 (lift (S n) O u) t3)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_:
111 T).(getl n c2 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u:
112 T).(\lambda (t: T).(ty3 g e u t)))) P (\lambda (x3: C).(\lambda (x4:
113 T).(\lambda (x5: T).(\lambda (_: (pc3 c2 (lift (S n) O x4) t3)).(\lambda
114 (H10: (getl n c2 (CHead x3 (Bind Abst) x4))).(\lambda (_: (ty3 g x3 x4
115 x5)).(let H12 \def (eq_ind C (CHead x0 (Bind Void) x2) (\lambda (c0: C).(getl
116 n c2 c0)) H6 (CHead x3 (Bind Abst) x4) (getl_mono c2 (CHead x0 (Bind Void)
117 x2) n H6 (CHead x3 (Bind Abst) x4) H10)) in (let H13 \def (eq_ind C (CHead x0
118 (Bind Void) x2) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop)
119 with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K
120 return (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return
121 (\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow False |
122 Void \Rightarrow True]) | (Flat _) \Rightarrow False])])) I (CHead x3 (Bind
123 Abst) x4) (getl_mono c2 (CHead x0 (Bind Void) x2) n H6 (CHead x3 (Bind Abst)
124 x4) H10)) in (False_ind P H13))))))))) H8)) (ty3_gen_lref g c2 t3 n H7)))))))
125 x1 H2))) H4)) (\lambda (H4: ((\forall (t3: T).((ty3 g x0 x2 t3) \to (\forall
126 (P: Prop).P))))).(or_intror (ex T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3)))
127 (\forall (t3: T).((ty3 g c2 (TLRef n) t3) \to (\forall (P: Prop).P)))
128 (\lambda (t3: T).(\lambda (H5: (ty3 g c2 (TLRef n) t3)).(\lambda (P:
129 Prop).(or_ind (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t:
130 T).(pc3 c2 (lift (S n) O t) t3)))) (\lambda (e: C).(\lambda (u: T).(\lambda
131 (_: T).(getl n c2 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
132 T).(\lambda (t: T).(ty3 g e u t))))) (ex3_3 C T T (\lambda (_: C).(\lambda
133 (u: T).(\lambda (_: T).(pc3 c2 (lift (S n) O u) t3)))) (\lambda (e:
134 C).(\lambda (u: T).(\lambda (_: T).(getl n c2 (CHead e (Bind Abst) u)))))
135 (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t))))) P (\lambda
136 (H6: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 c2
137 (lift (S n) O t) t3)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl
138 n c2 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t:
139 T).(ty3 g e u t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_:
140 T).(\lambda (t: T).(pc3 c2 (lift (S n) O t) t3)))) (\lambda (e: C).(\lambda
141 (u: T).(\lambda (_: T).(getl n c2 (CHead e (Bind Abbr) u))))) (\lambda (e:
142 C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t)))) P (\lambda (x3:
143 C).(\lambda (x4: T).(\lambda (x5: T).(\lambda (_: (pc3 c2 (lift (S n) O x5)
144 t3)).(\lambda (H8: (getl n c2 (CHead x3 (Bind Abbr) x4))).(\lambda (H9: (ty3
145 g x3 x4 x5)).(let H10 \def (eq_ind C (CHead x0 (Bind x1) x2) (\lambda (c0:
146 C).(getl n c2 c0)) H2 (CHead x3 (Bind Abbr) x4) (getl_mono c2 (CHead x0 (Bind
147 x1) x2) n H2 (CHead x3 (Bind Abbr) x4) H8)) in (let H11 \def (f_equal C C
148 (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
149 \Rightarrow x0 | (CHead c0 _ _) \Rightarrow c0])) (CHead x0 (Bind x1) x2)
150 (CHead x3 (Bind Abbr) x4) (getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead
151 x3 (Bind Abbr) x4) H8)) in ((let H12 \def (f_equal C B (\lambda (e: C).(match
152 e in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow x1 | (CHead _ k
153 _) \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
154 \Rightarrow b | (Flat _) \Rightarrow x1])])) (CHead x0 (Bind x1) x2) (CHead
155 x3 (Bind Abbr) x4) (getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead x3 (Bind
156 Abbr) x4) H8)) in ((let H13 \def (f_equal C T (\lambda (e: C).(match e in C
157 return (\lambda (_: C).T) with [(CSort _) \Rightarrow x2 | (CHead _ _ t)
158 \Rightarrow t])) (CHead x0 (Bind x1) x2) (CHead x3 (Bind Abbr) x4) (getl_mono
159 c2 (CHead x0 (Bind x1) x2) n H2 (CHead x3 (Bind Abbr) x4) H8)) in (\lambda
160 (_: (eq B x1 Abbr)).(\lambda (H15: (eq C x0 x3)).(let H16 \def (eq_ind_r T x4
161 (\lambda (t: T).(getl n c2 (CHead x3 (Bind Abbr) t))) H10 x2 H13) in (let H17
162 \def (eq_ind_r T x4 (\lambda (t: T).(ty3 g x3 t x5)) H9 x2 H13) in (let H18
163 \def (eq_ind_r C x3 (\lambda (c0: C).(getl n c2 (CHead c0 (Bind Abbr) x2)))
164 H16 x0 H15) in (let H19 \def (eq_ind_r C x3 (\lambda (c0: C).(ty3 g c0 x2
165 x5)) H17 x0 H15) in (H4 x5 H19 P)))))))) H12)) H11))))))))) H6)) (\lambda
166 (H6: (ex3_3 C T T (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(pc3 c2
167 (lift (S n) O u) t3)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl
168 n c2 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t:
169 T).(ty3 g e u t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (u:
170 T).(\lambda (_: T).(pc3 c2 (lift (S n) O u) t3)))) (\lambda (e: C).(\lambda
171 (u: T).(\lambda (_: T).(getl n c2 (CHead e (Bind Abst) u))))) (\lambda (e:
172 C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t)))) P (\lambda (x3:
173 C).(\lambda (x4: T).(\lambda (x5: T).(\lambda (H7: (pc3 c2 (lift (S n) O x4)
174 t3)).(\lambda (H8: (getl n c2 (CHead x3 (Bind Abst) x4))).(\lambda (H9: (ty3
175 g x3 x4 x5)).(let H10 \def (eq_ind C (CHead x0 (Bind x1) x2) (\lambda (c0:
176 C).(getl n c2 c0)) H2 (CHead x3 (Bind Abst) x4) (getl_mono c2 (CHead x0 (Bind
177 x1) x2) n H2 (CHead x3 (Bind Abst) x4) H8)) in (let H11 \def (f_equal C C
178 (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
179 \Rightarrow x0 | (CHead c0 _ _) \Rightarrow c0])) (CHead x0 (Bind x1) x2)
180 (CHead x3 (Bind Abst) x4) (getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead
181 x3 (Bind Abst) x4) H8)) in ((let H12 \def (f_equal C B (\lambda (e: C).(match
182 e in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow x1 | (CHead _ k
183 _) \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
184 \Rightarrow b | (Flat _) \Rightarrow x1])])) (CHead x0 (Bind x1) x2) (CHead
185 x3 (Bind Abst) x4) (getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead x3 (Bind
186 Abst) x4) H8)) in ((let H13 \def (f_equal C T (\lambda (e: C).(match e in C
187 return (\lambda (_: C).T) with [(CSort _) \Rightarrow x2 | (CHead _ _ t)
188 \Rightarrow t])) (CHead x0 (Bind x1) x2) (CHead x3 (Bind Abst) x4) (getl_mono
189 c2 (CHead x0 (Bind x1) x2) n H2 (CHead x3 (Bind Abst) x4) H8)) in (\lambda
190 (_: (eq B x1 Abst)).(\lambda (H15: (eq C x0 x3)).(let H16 \def (eq_ind_r T x4
191 (\lambda (t: T).(getl n c2 (CHead x3 (Bind Abst) t))) H10 x2 H13) in (let H17
192 \def (eq_ind_r T x4 (\lambda (t: T).(ty3 g x3 t x5)) H9 x2 H13) in (let H18
193 \def (eq_ind_r T x4 (\lambda (t: T).(pc3 c2 (lift (S n) O t) t3)) H7 x2 H13)
194 in (let H19 \def (eq_ind_r C x3 (\lambda (c0: C).(getl n c2 (CHead c0 (Bind
195 Abst) x2))) H16 x0 H15) in (let H20 \def (eq_ind_r C x3 (\lambda (c0: C).(ty3
196 g c0 x2 x5)) H17 x0 H15) in (H4 x5 H20 P))))))))) H12)) H11))))))))) H6))
197 (ty3_gen_lref g c2 t3 n H5))))))) H3)))))) H1)) (\lambda (H1: ((\forall (d:
198 C).((getl n c2 d) \to (\forall (P: Prop).P))))).(or_intror (ex T (\lambda
199 (t3: T).(ty3 g c2 (TLRef n) t3))) (\forall (t3: T).((ty3 g c2 (TLRef n) t3)
200 \to (\forall (P: Prop).P))) (\lambda (t3: T).(\lambda (H2: (ty3 g c2 (TLRef
201 n) t3)).(\lambda (P: Prop).(or_ind (ex3_3 C T T (\lambda (_: C).(\lambda (_:
202 T).(\lambda (t: T).(pc3 c2 (lift (S n) O t) t3)))) (\lambda (e: C).(\lambda
203 (u: T).(\lambda (_: T).(getl n c2 (CHead e (Bind Abbr) u))))) (\lambda (e:
204 C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t))))) (ex3_3 C T T (\lambda
205 (_: C).(\lambda (u: T).(\lambda (_: T).(pc3 c2 (lift (S n) O u) t3))))
206 (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c2 (CHead e (Bind
207 Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u
208 t))))) P (\lambda (H3: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda
209 (t: T).(pc3 c2 (lift (S n) O t) t3)))) (\lambda (e: C).(\lambda (u:
210 T).(\lambda (_: T).(getl n c2 (CHead e (Bind Abbr) u))))) (\lambda (e:
211 C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t)))))).(ex3_3_ind C T T
212 (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 c2 (lift (S n) O t)
213 t3)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c2 (CHead e
214 (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u
215 t)))) P (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3
216 c2 (lift (S n) O x2) t3)).(\lambda (H5: (getl n c2 (CHead x0 (Bind Abbr)
217 x1))).(\lambda (_: (ty3 g x0 x1 x2)).(H1 (CHead x0 (Bind Abbr) x1) H5
218 P))))))) H3)) (\lambda (H3: (ex3_3 C T T (\lambda (_: C).(\lambda (u:
219 T).(\lambda (_: T).(pc3 c2 (lift (S n) O u) t3)))) (\lambda (e: C).(\lambda
220 (u: T).(\lambda (_: T).(getl n c2 (CHead e (Bind Abst) u))))) (\lambda (e:
221 C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t)))))).(ex3_3_ind C T T
222 (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(pc3 c2 (lift (S n) O u)
223 t3)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c2 (CHead e
224 (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u
225 t)))) P (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3
226 c2 (lift (S n) O x1) t3)).(\lambda (H5: (getl n c2 (CHead x0 (Bind Abst)
227 x1))).(\lambda (_: (ty3 g x0 x1 x2)).(H1 (CHead x0 (Bind Abst) x1) H5
228 P))))))) H3)) (ty3_gen_lref g c2 t3 n H2))))))) H0))))) (\lambda (k:
229 K).(\lambda (t: T).(\lambda (_: ((((\forall (c1: C).(\forall (t3: T).((flt c1
230 t3 c2 t) \to (or (ex T (\lambda (t4: T).(ty3 g c1 t3 t4))) (\forall (t4:
231 T).((ty3 g c1 t3 t4) \to (\forall (P: Prop).P)))))))) \to (or (ex T (\lambda
232 (t3: T).(ty3 g c2 t t3))) (\forall (t3: T).((ty3 g c2 t t3) \to (\forall (P:
233 Prop).P))))))).(\lambda (t0: T).(\lambda (_: ((((\forall (c1: C).(\forall
234 (t3: T).((flt c1 t3 c2 t0) \to (or (ex T (\lambda (t4: T).(ty3 g c1 t3 t4)))
235 (\forall (t4: T).((ty3 g c1 t3 t4) \to (\forall (P: Prop).P)))))))) \to (or
236 (ex T (\lambda (t3: T).(ty3 g c2 t0 t3))) (\forall (t3: T).((ty3 g c2 t0 t3)
237 \to (\forall (P: Prop).P))))))).(\lambda (H1: ((\forall (c1: C).(\forall (t3:
238 T).((flt c1 t3 c2 (THead k t t0)) \to (or (ex T (\lambda (t4: T).(ty3 g c1 t3
239 t4))) (\forall (t4: T).((ty3 g c1 t3 t4) \to (\forall (P:
240 Prop).P))))))))).(K_ind (\lambda (k0: K).(((\forall (c1: C).(\forall (t3:
241 T).((flt c1 t3 c2 (THead k0 t t0)) \to (or (ex T (\lambda (t4: T).(ty3 g c1
242 t3 t4))) (\forall (t4: T).((ty3 g c1 t3 t4) \to (\forall (P: Prop).P))))))))
243 \to (or (ex T (\lambda (t3: T).(ty3 g c2 (THead k0 t t0) t3))) (\forall (t3:
244 T).((ty3 g c2 (THead k0 t t0) t3) \to (\forall (P: Prop).P)))))) (\lambda (b:
245 B).(\lambda (H2: ((\forall (c1: C).(\forall (t3: T).((flt c1 t3 c2 (THead
246 (Bind b) t t0)) \to (or (ex T (\lambda (t4: T).(ty3 g c1 t3 t4))) (\forall
247 (t4: T).((ty3 g c1 t3 t4) \to (\forall (P: Prop).P))))))))).(let H3 \def (H2
248 c2 t (flt_thead_sx (Bind b) c2 t t0)) in (or_ind (ex T (\lambda (t3: T).(ty3
249 g c2 t t3))) (\forall (t3: T).((ty3 g c2 t t3) \to (\forall (P: Prop).P)))
250 (or (ex T (\lambda (t3: T).(ty3 g c2 (THead (Bind b) t t0) t3))) (\forall
251 (t3: T).((ty3 g c2 (THead (Bind b) t t0) t3) \to (\forall (P: Prop).P))))
252 (\lambda (H4: (ex T (\lambda (t3: T).(ty3 g c2 t t3)))).(ex_ind T (\lambda
253 (t3: T).(ty3 g c2 t t3)) (or (ex T (\lambda (t3: T).(ty3 g c2 (THead (Bind b)
254 t t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Bind b) t t0) t3) \to
255 (\forall (P: Prop).P)))) (\lambda (x: T).(\lambda (H5: (ty3 g c2 t x)).(let
256 H6 \def (H2 (CHead c2 (Bind b) t) t0 (flt_shift (Bind b) c2 t t0)) in (or_ind
257 (ex T (\lambda (t3: T).(ty3 g (CHead c2 (Bind b) t) t0 t3))) (\forall (t3:
258 T).((ty3 g (CHead c2 (Bind b) t) t0 t3) \to (\forall (P: Prop).P))) (or (ex T
259 (\lambda (t3: T).(ty3 g c2 (THead (Bind b) t t0) t3))) (\forall (t3: T).((ty3
260 g c2 (THead (Bind b) t t0) t3) \to (\forall (P: Prop).P)))) (\lambda (H7: (ex
261 T (\lambda (t3: T).(ty3 g (CHead c2 (Bind b) t) t0 t3)))).(ex_ind T (\lambda
262 (t3: T).(ty3 g (CHead c2 (Bind b) t) t0 t3)) (or (ex T (\lambda (t3: T).(ty3
263 g c2 (THead (Bind b) t t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Bind b)
264 t t0) t3) \to (\forall (P: Prop).P)))) (\lambda (x0: T).(\lambda (H8: (ty3 g
265 (CHead c2 (Bind b) t) t0 x0)).(ex_ind T (\lambda (t3: T).(ty3 g (CHead c2
266 (Bind b) t) x0 t3)) (or (ex T (\lambda (t3: T).(ty3 g c2 (THead (Bind b) t
267 t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Bind b) t t0) t3) \to (\forall
268 (P: Prop).P)))) (\lambda (x1: T).(\lambda (H9: (ty3 g (CHead c2 (Bind b) t)
269 x0 x1)).(or_introl (ex T (\lambda (t3: T).(ty3 g c2 (THead (Bind b) t t0)
270 t3))) (\forall (t3: T).((ty3 g c2 (THead (Bind b) t t0) t3) \to (\forall (P:
271 Prop).P))) (ex_intro T (\lambda (t3: T).(ty3 g c2 (THead (Bind b) t t0) t3))
272 (THead (Bind b) t x0) (ty3_bind g c2 t x H5 b t0 x0 H8 x1 H9)))))
273 (ty3_correct g (CHead c2 (Bind b) t) t0 x0 H8)))) H7)) (\lambda (H7:
274 ((\forall (t3: T).((ty3 g (CHead c2 (Bind b) t) t0 t3) \to (\forall (P:
275 Prop).P))))).(or_intror (ex T (\lambda (t3: T).(ty3 g c2 (THead (Bind b) t
276 t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Bind b) t t0) t3) \to (\forall
277 (P: Prop).P))) (\lambda (t3: T).(\lambda (H8: (ty3 g c2 (THead (Bind b) t t0)
278 t3)).(\lambda (P: Prop).(ex4_3_ind T T T (\lambda (t4: T).(\lambda (_:
279 T).(\lambda (_: T).(pc3 c2 (THead (Bind b) t t4) t3)))) (\lambda (_:
280 T).(\lambda (t5: T).(\lambda (_: T).(ty3 g c2 t t5)))) (\lambda (t4:
281 T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c2 (Bind b) t) t0 t4))))
282 (\lambda (t4: T).(\lambda (_: T).(\lambda (t6: T).(ty3 g (CHead c2 (Bind b)
283 t) t4 t6)))) P (\lambda (x0: T).(\lambda (x1: T).(\lambda (x2: T).(\lambda
284 (_: (pc3 c2 (THead (Bind b) t x0) t3)).(\lambda (_: (ty3 g c2 t x1)).(\lambda
285 (H11: (ty3 g (CHead c2 (Bind b) t) t0 x0)).(\lambda (_: (ty3 g (CHead c2
286 (Bind b) t) x0 x2)).(H7 x0 H11 P)))))))) (ty3_gen_bind g b c2 t t0 t3
287 H8))))))) H6)))) H4)) (\lambda (H4: ((\forall (t3: T).((ty3 g c2 t t3) \to
288 (\forall (P: Prop).P))))).(or_intror (ex T (\lambda (t3: T).(ty3 g c2 (THead
289 (Bind b) t t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Bind b) t t0) t3)
290 \to (\forall (P: Prop).P))) (\lambda (t3: T).(\lambda (H5: (ty3 g c2 (THead
291 (Bind b) t t0) t3)).(\lambda (P: Prop).(ex4_3_ind T T T (\lambda (t4:
292 T).(\lambda (_: T).(\lambda (_: T).(pc3 c2 (THead (Bind b) t t4) t3))))
293 (\lambda (_: T).(\lambda (t5: T).(\lambda (_: T).(ty3 g c2 t t5)))) (\lambda
294 (t4: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c2 (Bind b) t) t0
295 t4)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (t6: T).(ty3 g (CHead c2
296 (Bind b) t) t4 t6)))) P (\lambda (x0: T).(\lambda (x1: T).(\lambda (x2:
297 T).(\lambda (_: (pc3 c2 (THead (Bind b) t x0) t3)).(\lambda (H7: (ty3 g c2 t
298 x1)).(\lambda (_: (ty3 g (CHead c2 (Bind b) t) t0 x0)).(\lambda (_: (ty3 g
299 (CHead c2 (Bind b) t) x0 x2)).(H4 x1 H7 P)))))))) (ty3_gen_bind g b c2 t t0
300 t3 H5))))))) H3)))) (\lambda (f: F).(\lambda (H2: ((\forall (c1: C).(\forall
301 (t3: T).((flt c1 t3 c2 (THead (Flat f) t t0)) \to (or (ex T (\lambda (t4:
302 T).(ty3 g c1 t3 t4))) (\forall (t4: T).((ty3 g c1 t3 t4) \to (\forall (P:
303 Prop).P))))))))).(F_ind (\lambda (f0: F).(((\forall (c1: C).(\forall (t3:
304 T).((flt c1 t3 c2 (THead (Flat f0) t t0)) \to (or (ex T (\lambda (t4: T).(ty3
305 g c1 t3 t4))) (\forall (t4: T).((ty3 g c1 t3 t4) \to (\forall (P:
306 Prop).P)))))))) \to (or (ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat f0) t
307 t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat f0) t t0) t3) \to (\forall
308 (P: Prop).P)))))) (\lambda (H3: ((\forall (c1: C).(\forall (t3: T).((flt c1
309 t3 c2 (THead (Flat Appl) t t0)) \to (or (ex T (\lambda (t4: T).(ty3 g c1 t3
310 t4))) (\forall (t4: T).((ty3 g c1 t3 t4) \to (\forall (P:
311 Prop).P))))))))).(let H4 \def (H3 c2 t (flt_thead_sx (Flat Appl) c2 t t0)) in
312 (or_ind (ex T (\lambda (t3: T).(ty3 g c2 t t3))) (\forall (t3: T).((ty3 g c2
313 t t3) \to (\forall (P: Prop).P))) (or (ex T (\lambda (t3: T).(ty3 g c2 (THead
314 (Flat Appl) t t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat Appl) t t0)
315 t3) \to (\forall (P: Prop).P)))) (\lambda (H5: (ex T (\lambda (t3: T).(ty3 g
316 c2 t t3)))).(ex_ind T (\lambda (t3: T).(ty3 g c2 t t3)) (or (ex T (\lambda
317 (t3: T).(ty3 g c2 (THead (Flat Appl) t t0) t3))) (\forall (t3: T).((ty3 g c2
318 (THead (Flat Appl) t t0) t3) \to (\forall (P: Prop).P)))) (\lambda (x:
319 T).(\lambda (H6: (ty3 g c2 t x)).(let H7 \def (H3 c2 t0 (flt_thead_dx (Flat
320 Appl) c2 t t0)) in (or_ind (ex T (\lambda (t3: T).(ty3 g c2 t0 t3))) (\forall
321 (t3: T).((ty3 g c2 t0 t3) \to (\forall (P: Prop).P))) (or (ex T (\lambda (t3:
322 T).(ty3 g c2 (THead (Flat Appl) t t0) t3))) (\forall (t3: T).((ty3 g c2
323 (THead (Flat Appl) t t0) t3) \to (\forall (P: Prop).P)))) (\lambda (H8: (ex T
324 (\lambda (t3: T).(ty3 g c2 t0 t3)))).(ex_ind T (\lambda (t3: T).(ty3 g c2 t0
325 t3)) (or (ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat Appl) t t0) t3)))
326 (\forall (t3: T).((ty3 g c2 (THead (Flat Appl) t t0) t3) \to (\forall (P:
327 Prop).P)))) (\lambda (x0: T).(\lambda (H9: (ty3 g c2 t0 x0)).(ex_ind T
328 (\lambda (t3: T).(ty3 g c2 x0 t3)) (or (ex T (\lambda (t3: T).(ty3 g c2
329 (THead (Flat Appl) t t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat Appl)
330 t t0) t3) \to (\forall (P: Prop).P)))) (\lambda (x1: T).(\lambda (H10: (ty3 g
331 c2 x0 x1)).(ex_ind T (\lambda (t3: T).(ty3 g c2 x t3)) (or (ex T (\lambda
332 (t3: T).(ty3 g c2 (THead (Flat Appl) t t0) t3))) (\forall (t3: T).((ty3 g c2
333 (THead (Flat Appl) t t0) t3) \to (\forall (P: Prop).P)))) (\lambda (x2:
334 T).(\lambda (H11: (ty3 g c2 x x2)).(let H12 \def (ty3_sn3 g c2 x x2 H11) in
335 (let H_x \def (nf2_sn3 c2 x H12) in (let H13 \def H_x in (ex2_ind T (\lambda
336 (u: T).(pr3 c2 x u)) (\lambda (u: T).(nf2 c2 u)) (or (ex T (\lambda (t3:
337 T).(ty3 g c2 (THead (Flat Appl) t t0) t3))) (\forall (t3: T).((ty3 g c2
338 (THead (Flat Appl) t t0) t3) \to (\forall (P: Prop).P)))) (\lambda (x3:
339 T).(\lambda (H14: (pr3 c2 x x3)).(\lambda (H15: (nf2 c2 x3)).(let H16 \def
340 (ty3_sred_pr3 c2 x x3 H14 g x2 H11) in (let H_x0 \def (pc3_abst_dec g c2 x0
341 x1 H10 x3 x2 H16) in (let H17 \def H_x0 in (or_ind (ex4_2 T T (\lambda (u:
342 T).(\lambda (_: T).(pc3 c2 x0 (THead (Bind Abst) x3 u)))) (\lambda (u:
343 T).(\lambda (v2: T).(ty3 g c2 (THead (Bind Abst) v2 u) x1))) (\lambda (_:
344 T).(\lambda (v2: T).(pr3 c2 x3 v2))) (\lambda (_: T).(\lambda (v2: T).(nf2 c2
345 v2)))) (\forall (u: T).((pc3 c2 x0 (THead (Bind Abst) x3 u)) \to (\forall (P:
346 Prop).P))) (or (ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat Appl) t t0)
347 t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat Appl) t t0) t3) \to (\forall
348 (P: Prop).P)))) (\lambda (H18: (ex4_2 T T (\lambda (u: T).(\lambda (_:
349 T).(pc3 c2 x0 (THead (Bind Abst) x3 u)))) (\lambda (u: T).(\lambda (v2:
350 T).(ty3 g c2 (THead (Bind Abst) v2 u) x1))) (\lambda (_: T).(\lambda (v2:
351 T).(pr3 c2 x3 v2))) (\lambda (_: T).(\lambda (v2: T).(nf2 c2
352 v2))))).(ex4_2_ind T T (\lambda (u: T).(\lambda (_: T).(pc3 c2 x0 (THead
353 (Bind Abst) x3 u)))) (\lambda (u: T).(\lambda (v2: T).(ty3 g c2 (THead (Bind
354 Abst) v2 u) x1))) (\lambda (_: T).(\lambda (v2: T).(pr3 c2 x3 v2))) (\lambda
355 (_: T).(\lambda (v2: T).(nf2 c2 v2))) (or (ex T (\lambda (t3: T).(ty3 g c2
356 (THead (Flat Appl) t t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat Appl)
357 t t0) t3) \to (\forall (P: Prop).P)))) (\lambda (x4: T).(\lambda (x5:
358 T).(\lambda (H19: (pc3 c2 x0 (THead (Bind Abst) x3 x4))).(\lambda (H20: (ty3
359 g c2 (THead (Bind Abst) x5 x4) x1)).(\lambda (H21: (pr3 c2 x3 x5)).(\lambda
360 (_: (nf2 c2 x5)).(let H_y \def (nf2_pr3_unfold c2 x3 x5 H21 H15) in (let H23
361 \def (eq_ind_r T x5 (\lambda (t3: T).(pr3 c2 x3 t3)) H21 x3 H_y) in (let H24
362 \def (eq_ind_r T x5 (\lambda (t3: T).(ty3 g c2 (THead (Bind Abst) t3 x4) x1))
363 H20 x3 H_y) in (or_introl (ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat Appl)
364 t t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat Appl) t t0) t3) \to
365 (\forall (P: Prop).P))) (ex_intro T (\lambda (t3: T).(ty3 g c2 (THead (Flat
366 Appl) t t0) t3)) (THead (Flat Appl) t (THead (Bind Abst) x3 x4)) (ty3_appl g
367 c2 t x3 (ty3_tred g c2 t x H6 x3 H14) t0 x4 (ty3_conv g c2 (THead (Bind Abst)
368 x3 x4) x1 H24 t0 x0 H9 H19))))))))))))) H18)) (\lambda (H18: ((\forall (u:
369 T).((pc3 c2 x0 (THead (Bind Abst) x3 u)) \to (\forall (P:
370 Prop).P))))).(or_intror (ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat Appl) t
371 t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat Appl) t t0) t3) \to
372 (\forall (P: Prop).P))) (\lambda (t3: T).(\lambda (H19: (ty3 g c2 (THead
373 (Flat Appl) t t0) t3)).(\lambda (P: Prop).(ex3_2_ind T T (\lambda (u:
374 T).(\lambda (t4: T).(pc3 c2 (THead (Flat Appl) t (THead (Bind Abst) u t4))
375 t3))) (\lambda (u: T).(\lambda (t4: T).(ty3 g c2 t0 (THead (Bind Abst) u
376 t4)))) (\lambda (u: T).(\lambda (_: T).(ty3 g c2 t u))) P (\lambda (x4:
377 T).(\lambda (x5: T).(\lambda (_: (pc3 c2 (THead (Flat Appl) t (THead (Bind
378 Abst) x4 x5)) t3)).(\lambda (H21: (ty3 g c2 t0 (THead (Bind Abst) x4
379 x5))).(\lambda (H22: (ty3 g c2 t x4)).(let H_y \def (ty3_unique g c2 t x4 H22
380 x H6) in (let H_y0 \def (ty3_unique g c2 t0 (THead (Bind Abst) x4 x5) H21 x0
381 H9) in (H18 x5 (pc3_t (THead (Bind Abst) x4 x5) c2 x0 (pc3_s c2 x0 (THead
382 (Bind Abst) x4 x5) H_y0) (THead (Bind Abst) x3 x5) (pc3_head_1 c2 x4 x3
383 (pc3_t x c2 x4 H_y x3 (pc3_pr3_r c2 x x3 H14)) (Bind Abst) x5)) P))))))))
384 (ty3_gen_appl g c2 t t0 t3 H19))))))) H17))))))) H13)))))) (ty3_correct g c2
385 t x H6)))) (ty3_correct g c2 t0 x0 H9)))) H8)) (\lambda (H8: ((\forall (t3:
386 T).((ty3 g c2 t0 t3) \to (\forall (P: Prop).P))))).(or_intror (ex T (\lambda
387 (t3: T).(ty3 g c2 (THead (Flat Appl) t t0) t3))) (\forall (t3: T).((ty3 g c2
388 (THead (Flat Appl) t t0) t3) \to (\forall (P: Prop).P))) (\lambda (t3:
389 T).(\lambda (H9: (ty3 g c2 (THead (Flat Appl) t t0) t3)).(\lambda (P:
390 Prop).(ex3_2_ind T T (\lambda (u: T).(\lambda (t4: T).(pc3 c2 (THead (Flat
391 Appl) t (THead (Bind Abst) u t4)) t3))) (\lambda (u: T).(\lambda (t4: T).(ty3
392 g c2 t0 (THead (Bind Abst) u t4)))) (\lambda (u: T).(\lambda (_: T).(ty3 g c2
393 t u))) P (\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (pc3 c2 (THead (Flat
394 Appl) t (THead (Bind Abst) x0 x1)) t3)).(\lambda (H11: (ty3 g c2 t0 (THead
395 (Bind Abst) x0 x1))).(\lambda (_: (ty3 g c2 t x0)).(H8 (THead (Bind Abst) x0
396 x1) H11 P)))))) (ty3_gen_appl g c2 t t0 t3 H9))))))) H7)))) H5)) (\lambda
397 (H5: ((\forall (t3: T).((ty3 g c2 t t3) \to (\forall (P:
398 Prop).P))))).(or_intror (ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat Appl) t
399 t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat Appl) t t0) t3) \to
400 (\forall (P: Prop).P))) (\lambda (t3: T).(\lambda (H6: (ty3 g c2 (THead (Flat
401 Appl) t t0) t3)).(\lambda (P: Prop).(ex3_2_ind T T (\lambda (u: T).(\lambda
402 (t4: T).(pc3 c2 (THead (Flat Appl) t (THead (Bind Abst) u t4)) t3))) (\lambda
403 (u: T).(\lambda (t4: T).(ty3 g c2 t0 (THead (Bind Abst) u t4)))) (\lambda (u:
404 T).(\lambda (_: T).(ty3 g c2 t u))) P (\lambda (x0: T).(\lambda (x1:
405 T).(\lambda (_: (pc3 c2 (THead (Flat Appl) t (THead (Bind Abst) x0 x1))
406 t3)).(\lambda (_: (ty3 g c2 t0 (THead (Bind Abst) x0 x1))).(\lambda (H9: (ty3
407 g c2 t x0)).(H5 x0 H9 P)))))) (ty3_gen_appl g c2 t t0 t3 H6))))))) H4)))
408 (\lambda (H3: ((\forall (c1: C).(\forall (t3: T).((flt c1 t3 c2 (THead (Flat
409 Cast) t t0)) \to (or (ex T (\lambda (t4: T).(ty3 g c1 t3 t4))) (\forall (t4:
410 T).((ty3 g c1 t3 t4) \to (\forall (P: Prop).P))))))))).(let H4 \def (H3 c2 t
411 (flt_thead_sx (Flat Cast) c2 t t0)) in (or_ind (ex T (\lambda (t3: T).(ty3 g
412 c2 t t3))) (\forall (t3: T).((ty3 g c2 t t3) \to (\forall (P: Prop).P))) (or
413 (ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat Cast) t t0) t3))) (\forall (t3:
414 T).((ty3 g c2 (THead (Flat Cast) t t0) t3) \to (\forall (P: Prop).P))))
415 (\lambda (H5: (ex T (\lambda (t3: T).(ty3 g c2 t t3)))).(ex_ind T (\lambda
416 (t3: T).(ty3 g c2 t t3)) (or (ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat
417 Cast) t t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat Cast) t t0) t3)
418 \to (\forall (P: Prop).P)))) (\lambda (x: T).(\lambda (H6: (ty3 g c2 t
419 x)).(let H7 \def (H3 c2 t0 (flt_thead_dx (Flat Cast) c2 t t0)) in (or_ind (ex
420 T (\lambda (t3: T).(ty3 g c2 t0 t3))) (\forall (t3: T).((ty3 g c2 t0 t3) \to
421 (\forall (P: Prop).P))) (or (ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat
422 Cast) t t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat Cast) t t0) t3)
423 \to (\forall (P: Prop).P)))) (\lambda (H8: (ex T (\lambda (t3: T).(ty3 g c2
424 t0 t3)))).(ex_ind T (\lambda (t3: T).(ty3 g c2 t0 t3)) (or (ex T (\lambda
425 (t3: T).(ty3 g c2 (THead (Flat Cast) t t0) t3))) (\forall (t3: T).((ty3 g c2
426 (THead (Flat Cast) t t0) t3) \to (\forall (P: Prop).P)))) (\lambda (x0:
427 T).(\lambda (H9: (ty3 g c2 t0 x0)).(ex_ind T (\lambda (t3: T).(ty3 g c2 x0
428 t3)) (or (ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat Cast) t t0) t3)))
429 (\forall (t3: T).((ty3 g c2 (THead (Flat Cast) t t0) t3) \to (\forall (P:
430 Prop).P)))) (\lambda (x1: T).(\lambda (H10: (ty3 g c2 x0 x1)).(let H_x \def
431 (pc3_dec g c2 x0 x1 H10 t x H6) in (let H11 \def H_x in (or_ind (pc3 c2 x0 t)
432 ((pc3 c2 x0 t) \to (\forall (P: Prop).P)) (or (ex T (\lambda (t3: T).(ty3 g
433 c2 (THead (Flat Cast) t t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat
434 Cast) t t0) t3) \to (\forall (P: Prop).P)))) (\lambda (H12: (pc3 c2 x0
435 t)).(or_introl (ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat Cast) t t0)
436 t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat Cast) t t0) t3) \to (\forall
437 (P: Prop).P))) (ex_intro T (\lambda (t3: T).(ty3 g c2 (THead (Flat Cast) t
438 t0) t3)) t (ty3_cast g c2 t0 t (ty3_conv g c2 t x H6 t0 x0 H9 H12) x H6))))
439 (\lambda (H12: (((pc3 c2 x0 t) \to (\forall (P: Prop).P)))).(or_intror (ex T
440 (\lambda (t3: T).(ty3 g c2 (THead (Flat Cast) t t0) t3))) (\forall (t3:
441 T).((ty3 g c2 (THead (Flat Cast) t t0) t3) \to (\forall (P: Prop).P)))
442 (\lambda (t3: T).(\lambda (H13: (ty3 g c2 (THead (Flat Cast) t t0)
443 t3)).(\lambda (P: Prop).(and_ind (pc3 c2 t t3) (ty3 g c2 t0 t) P (\lambda (_:
444 (pc3 c2 t t3)).(\lambda (H15: (ty3 g c2 t0 t)).(let H_y \def (ty3_unique g c2
445 t0 t H15 x0 H9) in (H12 (pc3_s c2 x0 t H_y) P)))) (ty3_gen_cast g c2 t0 t t3
446 H13))))))) H11))))) (ty3_correct g c2 t0 x0 H9)))) H8)) (\lambda (H8:
447 ((\forall (t3: T).((ty3 g c2 t0 t3) \to (\forall (P: Prop).P))))).(or_intror
448 (ex T (\lambda (t3: T).(ty3 g c2 (THead (Flat Cast) t t0) t3))) (\forall (t3:
449 T).((ty3 g c2 (THead (Flat Cast) t t0) t3) \to (\forall (P: Prop).P)))
450 (\lambda (t3: T).(\lambda (H9: (ty3 g c2 (THead (Flat Cast) t t0)
451 t3)).(\lambda (P: Prop).(and_ind (pc3 c2 t t3) (ty3 g c2 t0 t) P (\lambda (_:
452 (pc3 c2 t t3)).(\lambda (H11: (ty3 g c2 t0 t)).(H8 t H11 P))) (ty3_gen_cast g
453 c2 t0 t t3 H9))))))) H7)))) H5)) (\lambda (H5: ((\forall (t3: T).((ty3 g c2 t
454 t3) \to (\forall (P: Prop).P))))).(or_intror (ex T (\lambda (t3: T).(ty3 g c2
455 (THead (Flat Cast) t t0) t3))) (\forall (t3: T).((ty3 g c2 (THead (Flat Cast)
456 t t0) t3) \to (\forall (P: Prop).P))) (\lambda (t3: T).(\lambda (H6: (ty3 g
457 c2 (THead (Flat Cast) t t0) t3)).(\lambda (P: Prop).(and_ind (pc3 c2 t t3)
458 (ty3 g c2 t0 t) P (\lambda (_: (pc3 c2 t t3)).(\lambda (H8: (ty3 g c2 t0
459 t)).(ex_ind T (\lambda (t4: T).(ty3 g c2 t t4)) P (\lambda (x: T).(\lambda
460 (H9: (ty3 g c2 t x)).(H5 x H9 P))) (ty3_correct g c2 t0 t H8))))
461 (ty3_gen_cast g c2 t0 t t3 H6))))))) H4))) f H2))) k H1))))))) t2))) c t1))).