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