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