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