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