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