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