1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "LambdaDelta-1/csuba/fwd.ma".
19 include "LambdaDelta-1/drop/fwd.ma".
21 theorem csuba_drop_abbr:
22 \forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).((drop i
23 O c1 (CHead d1 (Bind Abbr) u)) \to (\forall (g: G).(\forall (c2: C).((csuba g
24 c1 c2) \to (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abbr) u)))
25 (\lambda (d2: C).(csuba g d1 d2))))))))))
27 \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (d1:
28 C).(\forall (u: T).((drop n O c1 (CHead d1 (Bind Abbr) u)) \to (\forall (g:
29 G).(\forall (c2: C).((csuba g c1 c2) \to (ex2 C (\lambda (d2: C).(drop n O c2
30 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))))))))))
31 (\lambda (c1: C).(\lambda (d1: C).(\lambda (u: T).(\lambda (H: (drop O O c1
32 (CHead d1 (Bind Abbr) u))).(\lambda (g: G).(\lambda (c2: C).(\lambda (H0:
33 (csuba g c1 c2)).(let H1 \def (eq_ind C c1 (\lambda (c: C).(csuba g c c2)) H0
34 (CHead d1 (Bind Abbr) u) (drop_gen_refl c1 (CHead d1 (Bind Abbr) u) H)) in
35 (let H_x \def (csuba_gen_abbr g d1 c2 u H1) in (let H2 \def H_x in (ex2_ind C
36 (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba
37 g d1 d2)) (ex2 C (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abbr) u)))
38 (\lambda (d2: C).(csuba g d1 d2))) (\lambda (x: C).(\lambda (H3: (eq C c2
39 (CHead x (Bind Abbr) u))).(\lambda (H4: (csuba g d1 x)).(eq_ind_r C (CHead x
40 (Bind Abbr) u) (\lambda (c: C).(ex2 C (\lambda (d2: C).(drop O O c (CHead d2
41 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (ex_intro2 C (\lambda
42 (d2: C).(drop O O (CHead x (Bind Abbr) u) (CHead d2 (Bind Abbr) u))) (\lambda
43 (d2: C).(csuba g d1 d2)) x (drop_refl (CHead x (Bind Abbr) u)) H4) c2 H3))))
44 H2))))))))))) (\lambda (n: nat).(\lambda (H: ((\forall (c1: C).(\forall (d1:
45 C).(\forall (u: T).((drop n O c1 (CHead d1 (Bind Abbr) u)) \to (\forall (g:
46 G).(\forall (c2: C).((csuba g c1 c2) \to (ex2 C (\lambda (d2: C).(drop n O c2
47 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
48 d2)))))))))))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (d1:
49 C).(\forall (u: T).((drop (S n) O c (CHead d1 (Bind Abbr) u)) \to (\forall
50 (g: G).(\forall (c2: C).((csuba g c c2) \to (ex2 C (\lambda (d2: C).(drop (S
51 n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))))))))))
52 (\lambda (n0: nat).(\lambda (d1: C).(\lambda (u: T).(\lambda (H0: (drop (S n)
53 O (CSort n0) (CHead d1 (Bind Abbr) u))).(\lambda (g: G).(\lambda (c2:
54 C).(\lambda (_: (csuba g (CSort n0) c2)).(and3_ind (eq C (CHead d1 (Bind
55 Abbr) u) (CSort n0)) (eq nat (S n) O) (eq nat O O) (ex2 C (\lambda (d2:
56 C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
57 d2))) (\lambda (_: (eq C (CHead d1 (Bind Abbr) u) (CSort n0))).(\lambda (H3:
58 (eq nat (S n) O)).(\lambda (_: (eq nat O O)).(let H5 \def (eq_ind nat (S n)
59 (\lambda (ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O
60 \Rightarrow False | (S _) \Rightarrow True])) I O H3) in (False_ind (ex2 C
61 (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
62 C).(csuba g d1 d2))) H5))))) (drop_gen_sort n0 (S n) O (CHead d1 (Bind Abbr)
63 u) H0))))))))) (\lambda (c: C).(\lambda (H0: ((\forall (d1: C).(\forall (u:
64 T).((drop (S n) O c (CHead d1 (Bind Abbr) u)) \to (\forall (g: G).(\forall
65 (c2: C).((csuba g c c2) \to (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead
66 d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))))))))))).(\lambda (k:
67 K).(\lambda (t: T).(\lambda (d1: C).(\lambda (u: T).(\lambda (H1: (drop (S n)
68 O (CHead c k t) (CHead d1 (Bind Abbr) u))).(\lambda (g: G).(\lambda (c2:
69 C).(\lambda (H2: (csuba g (CHead c k t) c2)).(K_ind (\lambda (k0: K).((csuba
70 g (CHead c k0 t) c2) \to ((drop (r k0 n) O c (CHead d1 (Bind Abbr) u)) \to
71 (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda
72 (d2: C).(csuba g d1 d2)))))) (\lambda (b: B).(\lambda (H3: (csuba g (CHead c
73 (Bind b) t) c2)).(\lambda (H4: (drop (r (Bind b) n) O c (CHead d1 (Bind Abbr)
74 u))).(B_ind (\lambda (b0: B).((csuba g (CHead c (Bind b0) t) c2) \to ((drop
75 (r (Bind b0) n) O c (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2:
76 C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
77 d2)))))) (\lambda (H5: (csuba g (CHead c (Bind Abbr) t) c2)).(\lambda (H6:
78 (drop (r (Bind Abbr) n) O c (CHead d1 (Bind Abbr) u))).(let H_x \def
79 (csuba_gen_abbr g c c2 t H5) in (let H7 \def H_x in (ex2_ind C (\lambda (d2:
80 C).(eq C c2 (CHead d2 (Bind Abbr) t))) (\lambda (d2: C).(csuba g c d2)) (ex2
81 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
82 C).(csuba g d1 d2))) (\lambda (x: C).(\lambda (H8: (eq C c2 (CHead x (Bind
83 Abbr) t))).(\lambda (H9: (csuba g c x)).(eq_ind_r C (CHead x (Bind Abbr) t)
84 (\lambda (c0: C).(ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind
85 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (let H10 \def (H c d1 u H6 g x
86 H9) in (ex2_ind C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abbr) u)))
87 (\lambda (d2: C).(csuba g d1 d2)) (ex2 C (\lambda (d2: C).(drop (S n) O
88 (CHead x (Bind Abbr) t) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g
89 d1 d2))) (\lambda (x0: C).(\lambda (H11: (drop n O x (CHead x0 (Bind Abbr)
90 u))).(\lambda (H12: (csuba g d1 x0)).(let H13 \def (refl_equal nat (r (Bind
91 Abbr) n)) in (let H14 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O x
92 (CHead x0 (Bind Abbr) u))) H11 (r (Bind Abbr) n) H13) in (ex_intro2 C
93 (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abbr)
94 u))) (\lambda (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Abbr) n x (CHead
95 x0 (Bind Abbr) u) H14 t) H12)))))) H10)) c2 H8)))) H7))))) (\lambda (H5:
96 (csuba g (CHead c (Bind Abst) t) c2)).(\lambda (H6: (drop (r (Bind Abst) n) O
97 c (CHead d1 (Bind Abbr) u))).(let H_x \def (csuba_gen_abst g c c2 t H5) in
98 (let H7 \def H_x in (or_ind (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind
99 Abst) t))) (\lambda (d2: C).(csuba g c d2))) (ex4_3 C T A (\lambda (d2:
100 C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2)))))
101 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g c d2)))) (\lambda
102 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g c t (asucc g a))))) (\lambda
103 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex2 C
104 (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
105 C).(csuba g d1 d2))) (\lambda (H8: (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2
106 (Bind Abst) t))) (\lambda (d2: C).(csuba g c d2)))).(ex2_ind C (\lambda (d2:
107 C).(eq C c2 (CHead d2 (Bind Abst) t))) (\lambda (d2: C).(csuba g c d2)) (ex2
108 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
109 C).(csuba g d1 d2))) (\lambda (x: C).(\lambda (H9: (eq C c2 (CHead x (Bind
110 Abst) t))).(\lambda (H10: (csuba g c x)).(eq_ind_r C (CHead x (Bind Abst) t)
111 (\lambda (c0: C).(ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind
112 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (let H11 \def (H c d1 u H6 g x
113 H10) in (ex2_ind C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abbr) u)))
114 (\lambda (d2: C).(csuba g d1 d2)) (ex2 C (\lambda (d2: C).(drop (S n) O
115 (CHead x (Bind Abst) t) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g
116 d1 d2))) (\lambda (x0: C).(\lambda (H12: (drop n O x (CHead x0 (Bind Abbr)
117 u))).(\lambda (H13: (csuba g d1 x0)).(let H14 \def (refl_equal nat (r (Bind
118 Abbr) n)) in (let H15 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O x
119 (CHead x0 (Bind Abbr) u))) H12 (r (Bind Abbr) n) H14) in (ex_intro2 C
120 (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abbr)
121 u))) (\lambda (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Abst) n x (CHead
122 x0 (Bind Abbr) u) H15 t) H13)))))) H11)) c2 H9)))) H8)) (\lambda (H8: (ex4_3
123 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2
124 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
125 c d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g c t (asucc
126 g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
127 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
128 A).(eq C c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
129 T).(\lambda (_: A).(csuba g c d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda
130 (a: A).(arity g c t (asucc g a))))) (\lambda (d2: C).(\lambda (u2:
131 T).(\lambda (a: A).(arity g d2 u2 a)))) (ex2 C (\lambda (d2: C).(drop (S n) O
132 c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) (\lambda
133 (x0: C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H9: (eq C c2 (CHead x0
134 (Bind Abbr) x1))).(\lambda (H10: (csuba g c x0)).(\lambda (_: (arity g c t
135 (asucc g x2))).(\lambda (_: (arity g x0 x1 x2)).(eq_ind_r C (CHead x0 (Bind
136 Abbr) x1) (\lambda (c0: C).(ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2
137 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (let H13 \def (H c d1 u
138 H6 g x0 H10) in (ex2_ind C (\lambda (d2: C).(drop n O x0 (CHead d2 (Bind
139 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) (ex2 C (\lambda (d2: C).(drop (S
140 n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abbr) u))) (\lambda (d2:
141 C).(csuba g d1 d2))) (\lambda (x: C).(\lambda (H14: (drop n O x0 (CHead x
142 (Bind Abbr) u))).(\lambda (H15: (csuba g d1 x)).(let H16 \def (refl_equal nat
143 (r (Bind Abbr) n)) in (let H17 \def (eq_ind nat n (\lambda (n0: nat).(drop n0
144 O x0 (CHead x (Bind Abbr) u))) H14 (r (Bind Abbr) n) H16) in (ex_intro2 C
145 (\lambda (d2: C).(drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind
146 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) x (drop_drop (Bind Abbr) n x0
147 (CHead x (Bind Abbr) u) H17 x1) H15)))))) H13)) c2 H9)))))))) H8)) H7)))))
148 (\lambda (H5: (csuba g (CHead c (Bind Void) t) c2)).(\lambda (H6: (drop (r
149 (Bind Void) n) O c (CHead d1 (Bind Abbr) u))).(let H_x \def (csuba_gen_void g
150 c c2 t H5) in (let H7 \def H_x in (ex2_ind C (\lambda (d2: C).(eq C c2 (CHead
151 d2 (Bind Void) t))) (\lambda (d2: C).(csuba g c d2)) (ex2 C (\lambda (d2:
152 C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
153 d2))) (\lambda (x: C).(\lambda (H8: (eq C c2 (CHead x (Bind Void)
154 t))).(\lambda (H9: (csuba g c x)).(eq_ind_r C (CHead x (Bind Void) t)
155 (\lambda (c0: C).(ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind
156 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (let H10 \def (H c d1 u H6 g x
157 H9) in (ex2_ind C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abbr) u)))
158 (\lambda (d2: C).(csuba g d1 d2)) (ex2 C (\lambda (d2: C).(drop (S n) O
159 (CHead x (Bind Void) t) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g
160 d1 d2))) (\lambda (x0: C).(\lambda (H11: (drop n O x (CHead x0 (Bind Abbr)
161 u))).(\lambda (H12: (csuba g d1 x0)).(let H13 \def (refl_equal nat (r (Bind
162 Abbr) n)) in (let H14 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O x
163 (CHead x0 (Bind Abbr) u))) H11 (r (Bind Abbr) n) H13) in (ex_intro2 C
164 (\lambda (d2: C).(drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abbr)
165 u))) (\lambda (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Void) n x (CHead
166 x0 (Bind Abbr) u) H14 t) H12)))))) H10)) c2 H8)))) H7))))) b H3 H4))))
167 (\lambda (f: F).(\lambda (H3: (csuba g (CHead c (Flat f) t) c2)).(\lambda
168 (H4: (drop (r (Flat f) n) O c (CHead d1 (Bind Abbr) u))).(let H_x \def
169 (csuba_gen_flat g c c2 t f H3) in (let H5 \def H_x in (ex2_2_ind C T (\lambda
170 (d2: C).(\lambda (u2: T).(eq C c2 (CHead d2 (Flat f) u2)))) (\lambda (d2:
171 C).(\lambda (_: T).(csuba g c d2))) (ex2 C (\lambda (d2: C).(drop (S n) O c2
172 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) (\lambda (x0:
173 C).(\lambda (x1: T).(\lambda (H6: (eq C c2 (CHead x0 (Flat f) x1))).(\lambda
174 (H7: (csuba g c x0)).(eq_ind_r C (CHead x0 (Flat f) x1) (\lambda (c0: C).(ex2
175 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
176 C).(csuba g d1 d2)))) (let H8 \def (H0 d1 u H4 g x0 H7) in (ex2_ind C
177 (\lambda (d2: C).(drop (S n) O x0 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
178 C).(csuba g d1 d2)) (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Flat f)
179 x1) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) (\lambda
180 (x: C).(\lambda (H9: (drop (S n) O x0 (CHead x (Bind Abbr) u))).(\lambda
181 (H10: (csuba g d1 x)).(ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x0
182 (Flat f) x1) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) x
183 (drop_drop (Flat f) n x0 (CHead x (Bind Abbr) u) H9 x1) H10)))) H8)) c2
184 H6))))) H5)))))) k H2 (drop_gen_drop k c (CHead d1 (Bind Abbr) u) t n
185 H1)))))))))))) c1)))) i).
187 theorem csuba_drop_abst:
188 \forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).((drop i
189 O c1 (CHead d1 (Bind Abst) u1)) \to (\forall (g: G).(\forall (c2: C).((csuba
190 g c1 c2) \to (or (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abst)
191 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
192 C).(\lambda (u2: T).(\lambda (_: A).(drop i O c2 (CHead d2 (Bind Abbr)
193 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
194 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
195 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
198 \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (d1:
199 C).(\forall (u1: T).((drop n O c1 (CHead d1 (Bind Abst) u1)) \to (\forall (g:
200 G).(\forall (c2: C).((csuba g c1 c2) \to (or (ex2 C (\lambda (d2: C).(drop n
201 O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C
202 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O c2 (CHead d2
203 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
204 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
205 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
206 u2 a)))))))))))))) (\lambda (c1: C).(\lambda (d1: C).(\lambda (u1:
207 T).(\lambda (H: (drop O O c1 (CHead d1 (Bind Abst) u1))).(\lambda (g:
208 G).(\lambda (c2: C).(\lambda (H0: (csuba g c1 c2)).(let H1 \def (eq_ind C c1
209 (\lambda (c: C).(csuba g c c2)) H0 (CHead d1 (Bind Abst) u1) (drop_gen_refl
210 c1 (CHead d1 (Bind Abst) u1) H)) in (let H_x \def (csuba_gen_abst g d1 c2 u1
211 H1) in (let H2 \def H_x in (or_ind (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2
212 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
213 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr)
214 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
215 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
216 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
217 a))))) (or (ex2 C (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abst) u1)))
218 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
219 (u2: T).(\lambda (_: A).(drop O O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda
220 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
221 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
222 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (H3:
223 (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
224 C).(csuba g d1 d2)))).(ex2_ind C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind
225 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) (or (ex2 C (\lambda (d2:
226 C).(drop O O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
227 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O
228 O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
229 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
230 A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
231 (a: A).(arity g d2 u2 a)))))) (\lambda (x: C).(\lambda (H4: (eq C c2 (CHead x
232 (Bind Abst) u1))).(\lambda (H5: (csuba g d1 x)).(eq_ind_r C (CHead x (Bind
233 Abst) u1) (\lambda (c: C).(or (ex2 C (\lambda (d2: C).(drop O O c (CHead d2
234 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
235 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O c (CHead d2 (Bind Abbr)
236 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
237 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
238 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
239 a))))))) (or_introl (ex2 C (\lambda (d2: C).(drop O O (CHead x (Bind Abst)
240 u1) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T
241 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O (CHead x (Bind
242 Abst) u1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
243 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
244 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
245 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex_intro2 C (\lambda (d2:
246 C).(drop O O (CHead x (Bind Abst) u1) (CHead d2 (Bind Abst) u1))) (\lambda
247 (d2: C).(csuba g d1 d2)) x (drop_refl (CHead x (Bind Abst) u1)) H5)) c2
248 H4)))) H3)) (\lambda (H3: (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
249 T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
250 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
251 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
252 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))).(ex4_3_ind C
253 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2
254 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
255 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
256 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
257 u2 a)))) (or (ex2 C (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abst) u1)))
258 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
259 (u2: T).(\lambda (_: A).(drop O O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda
260 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
261 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
262 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x0:
263 C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H4: (eq C c2 (CHead x0 (Bind
264 Abbr) x1))).(\lambda (H5: (csuba g d1 x0)).(\lambda (H6: (arity g d1 u1
265 (asucc g x2))).(\lambda (H7: (arity g x0 x1 x2)).(eq_ind_r C (CHead x0 (Bind
266 Abbr) x1) (\lambda (c: C).(or (ex2 C (\lambda (d2: C).(drop O O c (CHead d2
267 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
268 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O c (CHead d2 (Bind Abbr)
269 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
270 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
271 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
272 a))))))) (or_intror (ex2 C (\lambda (d2: C).(drop O O (CHead x0 (Bind Abbr)
273 x1) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T
274 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O (CHead x0 (Bind
275 Abbr) x1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
276 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
277 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
278 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex4_3_intro C T A (\lambda
279 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O (CHead x0 (Bind Abbr) x1)
280 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
281 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
282 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
283 A).(arity g d2 u2 a)))) x0 x1 x2 (drop_refl (CHead x0 (Bind Abbr) x1)) H5 H6
284 H7)) c2 H4)))))))) H3)) H2))))))))))) (\lambda (n: nat).(\lambda (H:
285 ((\forall (c1: C).(\forall (d1: C).(\forall (u1: T).((drop n O c1 (CHead d1
286 (Bind Abst) u1)) \to (\forall (g: G).(\forall (c2: C).((csuba g c1 c2) \to
287 (or (ex2 C (\lambda (d2: C).(drop n O c2 (CHead d2 (Bind Abst) u1))) (\lambda
288 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
289 T).(\lambda (_: A).(drop n O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
290 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
291 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
292 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
293 a))))))))))))))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (d1:
294 C).(\forall (u1: T).((drop (S n) O c (CHead d1 (Bind Abst) u1)) \to (\forall
295 (g: G).(\forall (c2: C).((csuba g c c2) \to (or (ex2 C (\lambda (d2: C).(drop
296 (S n) O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
297 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O
298 c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
299 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
300 A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
301 (a: A).(arity g d2 u2 a))))))))))))) (\lambda (n0: nat).(\lambda (d1:
302 C).(\lambda (u1: T).(\lambda (H0: (drop (S n) O (CSort n0) (CHead d1 (Bind
303 Abst) u1))).(\lambda (g: G).(\lambda (c2: C).(\lambda (_: (csuba g (CSort n0)
304 c2)).(and3_ind (eq C (CHead d1 (Bind Abst) u1) (CSort n0)) (eq nat (S n) O)
305 (eq nat O O) (or (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind
306 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
307 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c2 (CHead d2 (Bind Abbr)
308 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
309 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
310 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
311 a)))))) (\lambda (_: (eq C (CHead d1 (Bind Abst) u1) (CSort n0))).(\lambda
312 (H3: (eq nat (S n) O)).(\lambda (_: (eq nat O O)).(let H5 \def (eq_ind nat (S
313 n) (\lambda (ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O
314 \Rightarrow False | (S _) \Rightarrow True])) I O H3) in (False_ind (or (ex2
315 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
316 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
317 (_: A).(drop (S n) O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
318 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
319 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
320 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) H5)))))
321 (drop_gen_sort n0 (S n) O (CHead d1 (Bind Abst) u1) H0))))))))) (\lambda (c:
322 C).(\lambda (H0: ((\forall (d1: C).(\forall (u1: T).((drop (S n) O c (CHead
323 d1 (Bind Abst) u1)) \to (\forall (g: G).(\forall (c2: C).((csuba g c c2) \to
324 (or (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u1)))
325 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
326 (u2: T).(\lambda (_: A).(drop (S n) O c2 (CHead d2 (Bind Abbr) u2)))))
327 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
328 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
329 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
330 a)))))))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (d1: C).(\lambda
331 (u1: T).(\lambda (H1: (drop (S n) O (CHead c k t) (CHead d1 (Bind Abst)
332 u1))).(\lambda (g: G).(\lambda (c2: C).(\lambda (H2: (csuba g (CHead c k t)
333 c2)).(K_ind (\lambda (k0: K).((csuba g (CHead c k0 t) c2) \to ((drop (r k0 n)
334 O c (CHead d1 (Bind Abst) u1)) \to (or (ex2 C (\lambda (d2: C).(drop (S n) O
335 c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T
336 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c2 (CHead
337 d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
338 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
339 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
340 A).(arity g d2 u2 a))))))))) (\lambda (b: B).(\lambda (H3: (csuba g (CHead c
341 (Bind b) t) c2)).(\lambda (H4: (drop (r (Bind b) n) O c (CHead d1 (Bind Abst)
342 u1))).(B_ind (\lambda (b0: B).((csuba g (CHead c (Bind b0) t) c2) \to ((drop
343 (r (Bind b0) n) O c (CHead d1 (Bind Abst) u1)) \to (or (ex2 C (\lambda (d2:
344 C).(drop (S n) O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
345 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S
346 n) O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
347 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
348 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
349 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))))))) (\lambda (H5: (csuba g
350 (CHead c (Bind Abbr) t) c2)).(\lambda (H6: (drop (r (Bind Abbr) n) O c (CHead
351 d1 (Bind Abst) u1))).(let H_x \def (csuba_gen_abbr g c c2 t H5) in (let H7
352 \def H_x in (ex2_ind C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abbr) t)))
353 (\lambda (d2: C).(csuba g c d2)) (or (ex2 C (\lambda (d2: C).(drop (S n) O c2
354 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
355 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) 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)))))) (\lambda (x: C).(\lambda (H8: (eq C c2 (CHead x (Bind Abbr)
360 t))).(\lambda (H9: (csuba g c x)).(eq_ind_r C (CHead x (Bind Abbr) t)
361 (\lambda (c0: C).(or (ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind
362 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
363 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c0 (CHead d2 (Bind Abbr)
364 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
365 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
366 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
367 a))))))) (let H10 \def (H c d1 u1 H6 g x H9) in (or_ind (ex2 C (\lambda (d2:
368 C).(drop n O x (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
369 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O x
370 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
371 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
372 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
373 A).(arity g d2 u2 a))))) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x
374 (Bind Abbr) t) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
375 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O
376 (CHead x (Bind Abbr) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
377 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
378 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
379 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda
380 (H11: (ex2 C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abst) u1)))
381 (\lambda (d2: C).(csuba g d1 d2)))).(ex2_ind C (\lambda (d2: C).(drop n O x
382 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) (or (ex2 C
383 (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst)
384 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
385 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Abbr) t)
386 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
387 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
388 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
389 A).(arity g d2 u2 a)))))) (\lambda (x0: C).(\lambda (H12: (drop n O x (CHead
390 x0 (Bind Abst) u1))).(\lambda (H13: (csuba g d1 x0)).(let H14 \def
391 (refl_equal nat (r (Bind Abbr) n)) in (let H15 \def (eq_ind nat n (\lambda
392 (n0: nat).(drop n0 O x (CHead x0 (Bind Abst) u1))) H12 (r (Bind Abbr) n) H14)
393 in (or_introl (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abbr) t)
394 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
395 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x
396 (Bind Abbr) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
397 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
398 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
399 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex_intro2 C (\lambda (d2:
400 C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1))) (\lambda
401 (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Abbr) n x (CHead x0 (Bind Abst)
402 u1) H15 t) H13))))))) H11)) (\lambda (H11: (ex4_3 C T A (\lambda (d2:
403 C).(\lambda (u2: T).(\lambda (_: A).(drop n O x (CHead d2 (Bind Abbr) u2)))))
404 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
405 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
406 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
407 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
408 A).(drop n O x (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
409 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
410 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
411 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) (or (ex2 C (\lambda (d2:
412 C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1))) (\lambda
413 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
414 T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind
415 Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1
416 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc
417 g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
418 a)))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H12:
419 (drop n O x (CHead x0 (Bind Abbr) x1))).(\lambda (H13: (csuba g d1
420 x0)).(\lambda (H14: (arity g d1 u1 (asucc g x2))).(\lambda (H15: (arity g x0
421 x1 x2)).(let H16 \def (refl_equal nat (r (Bind Abbr) n)) in (let H17 \def
422 (eq_ind nat n (\lambda (n0: nat).(drop n0 O x (CHead x0 (Bind Abbr) x1))) H12
423 (r (Bind Abbr) n) H16) in (or_intror (ex2 C (\lambda (d2: C).(drop (S n) O
424 (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g
425 d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop
426 (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
427 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
428 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
429 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex4_3_intro C
430 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x
431 (Bind Abbr) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
432 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
433 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
434 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) x0 x1 x2 (drop_drop (Bind Abbr)
435 n x (CHead x0 (Bind Abbr) x1) H17 t) H13 H14 H15))))))))))) H11)) H10)) c2
436 H8)))) H7))))) (\lambda (H5: (csuba g (CHead c (Bind Abst) t) c2)).(\lambda
437 (H6: (drop (r (Bind Abst) n) O c (CHead d1 (Bind Abst) u1))).(let H_x \def
438 (csuba_gen_abst g c c2 t H5) in (let H7 \def H_x in (or_ind (ex2 C (\lambda
439 (d2: C).(eq C c2 (CHead d2 (Bind Abst) t))) (\lambda (d2: C).(csuba g c d2)))
440 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2
441 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
442 A).(csuba g c d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g
443 c t (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity
444 g d2 u2 a))))) (or (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind
445 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
446 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c2 (CHead d2 (Bind Abbr)
447 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
448 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
449 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
450 a)))))) (\lambda (H8: (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst)
451 t))) (\lambda (d2: C).(csuba g c d2)))).(ex2_ind C (\lambda (d2: C).(eq C c2
452 (CHead d2 (Bind Abst) t))) (\lambda (d2: C).(csuba g c d2)) (or (ex2 C
453 (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
454 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
455 (_: A).(drop (S n) O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
456 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
457 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
458 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x:
459 C).(\lambda (H9: (eq C c2 (CHead x (Bind Abst) t))).(\lambda (H10: (csuba g c
460 x)).(eq_ind_r C (CHead x (Bind Abst) t) (\lambda (c0: C).(or (ex2 C (\lambda
461 (d2: C).(drop (S n) O c0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba
462 g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
463 A).(drop (S n) O c0 (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))))))) (let H11 \def (H c d1 u1 H6 g
467 x H10) in (or_ind (ex2 C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abst)
468 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
469 C).(\lambda (u2: T).(\lambda (_: A).(drop n O x (CHead d2 (Bind Abbr) u2)))))
470 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
471 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
472 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (or
473 (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind
474 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
475 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Abst) t)
476 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
477 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
478 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
479 A).(arity g d2 u2 a)))))) (\lambda (H12: (ex2 C (\lambda (d2: C).(drop n O x
480 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))).(ex2_ind C
481 (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abst) u1))) (\lambda (d2:
482 C).(csuba g d1 d2)) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind
483 Abst) t) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
484 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O
485 (CHead x (Bind Abst) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
486 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
487 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
488 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x0:
489 C).(\lambda (H13: (drop n O x (CHead x0 (Bind Abst) u1))).(\lambda (H14:
490 (csuba g d1 x0)).(let H15 \def (refl_equal nat (r (Bind Abbr) n)) in (let H16
491 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O x (CHead x0 (Bind Abst)
492 u1))) H13 (r (Bind Abbr) n) H15) in (or_introl (ex2 C (\lambda (d2: C).(drop
493 (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1))) (\lambda (d2:
494 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
495 (_: A).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abbr) u2)))))
496 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
497 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
498 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))
499 (ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2
500 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Abst)
501 n x (CHead x0 (Bind Abst) u1) H16 t) H14))))))) H12)) (\lambda (H12: (ex4_3 C
502 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O x (CHead d2
503 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
504 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
505 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
506 u2 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
507 A).(drop n O x (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
508 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
509 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
510 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) (or (ex2 C (\lambda (d2:
511 C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1))) (\lambda
512 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
513 T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind
514 Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1
515 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc
516 g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
517 a)))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H13:
518 (drop n O x (CHead x0 (Bind Abbr) x1))).(\lambda (H14: (csuba g d1
519 x0)).(\lambda (H15: (arity g d1 u1 (asucc g x2))).(\lambda (H16: (arity g x0
520 x1 x2)).(let H17 \def (refl_equal nat (r (Bind Abbr) n)) in (let H18 \def
521 (eq_ind nat n (\lambda (n0: nat).(drop n0 O x (CHead x0 (Bind Abbr) x1))) H13
522 (r (Bind Abbr) n) H17) in (or_intror (ex2 C (\lambda (d2: C).(drop (S n) O
523 (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g
524 d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop
525 (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
526 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
527 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
528 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex4_3_intro C
529 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x
530 (Bind Abst) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
531 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
532 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
533 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) x0 x1 x2 (drop_drop (Bind Abst)
534 n x (CHead x0 (Bind Abbr) x1) H18 t) H14 H15 H16))))))))))) H12)) H11)) c2
535 H9)))) H8)) (\lambda (H8: (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
536 T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
537 C).(\lambda (_: T).(\lambda (_: A).(csuba g c d2)))) (\lambda (_: C).(\lambda
538 (_: T).(\lambda (a: A).(arity g c t (asucc g a))))) (\lambda (d2: C).(\lambda
539 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))).(ex4_3_ind C T A (\lambda (d2:
540 C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2)))))
541 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g c d2)))) (\lambda
542 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g c t (asucc g a))))) (\lambda
543 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) (or (ex2 C
544 (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
545 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
546 (_: A).(drop (S n) O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
547 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
548 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
549 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x0:
550 C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H9: (eq C c2 (CHead x0 (Bind
551 Abbr) x1))).(\lambda (H10: (csuba g c x0)).(\lambda (_: (arity g c t (asucc g
552 x2))).(\lambda (_: (arity g x0 x1 x2)).(eq_ind_r C (CHead x0 (Bind Abbr) x1)
553 (\lambda (c0: C).(or (ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind
554 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
555 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c0 (CHead d2 (Bind Abbr)
556 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
557 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
558 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
559 a))))))) (let H13 \def (H c d1 u1 H6 g x0 H10) in (or_ind (ex2 C (\lambda
560 (d2: C).(drop n O x0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
561 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n
562 O x0 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
563 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
564 A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
565 (a: A).(arity g d2 u2 a))))) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead
566 x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
567 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S
568 n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
569 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
570 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
571 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda
572 (H14: (ex2 C (\lambda (d2: C).(drop n O x0 (CHead d2 (Bind Abst) u1)))
573 (\lambda (d2: C).(csuba g d1 d2)))).(ex2_ind C (\lambda (d2: C).(drop n O x0
574 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) (or (ex2 C
575 (\lambda (d2: C).(drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind
576 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
577 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0 (Bind Abbr) x1)
578 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
579 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
580 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
581 A).(arity g d2 u2 a)))))) (\lambda (x: C).(\lambda (H15: (drop n O x0 (CHead
582 x (Bind Abst) u1))).(\lambda (H16: (csuba g d1 x)).(let H17 \def (refl_equal
583 nat (r (Bind Abbr) n)) in (let H18 \def (eq_ind nat n (\lambda (n0:
584 nat).(drop n0 O x0 (CHead x (Bind Abst) u1))) H15 (r (Bind Abbr) n) H17) in
585 (or_introl (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Bind Abbr) x1)
586 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
587 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0
588 (Bind Abbr) x1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
589 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
590 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
591 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex_intro2 C (\lambda (d2:
592 C).(drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)))
593 (\lambda (d2: C).(csuba g d1 d2)) x (drop_drop (Bind Abbr) n x0 (CHead x
594 (Bind Abst) u1) H18 x1) H16))))))) H14)) (\lambda (H14: (ex4_3 C T A (\lambda
595 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O x0 (CHead d2 (Bind Abbr)
596 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
597 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
598 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
599 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
600 A).(drop n O x0 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
601 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
602 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
603 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) (or (ex2 C (\lambda (d2:
604 C).(drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)))
605 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
606 (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2
607 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
608 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
609 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
610 u2 a)))))) (\lambda (x3: C).(\lambda (x4: T).(\lambda (x5: A).(\lambda (H15:
611 (drop n O x0 (CHead x3 (Bind Abbr) x4))).(\lambda (H16: (csuba g d1
612 x3)).(\lambda (H17: (arity g d1 u1 (asucc g x5))).(\lambda (H18: (arity g x3
613 x4 x5)).(let H19 \def (refl_equal nat (r (Bind Abbr) n)) in (let H20 \def
614 (eq_ind nat n (\lambda (n0: nat).(drop n0 O x0 (CHead x3 (Bind Abbr) x4)))
615 H15 (r (Bind Abbr) n) H19) in (or_intror (ex2 C (\lambda (d2: C).(drop (S n)
616 O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1))) (\lambda (d2:
617 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
618 (_: A).(drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abbr) u2)))))
619 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
620 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
621 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))
622 (ex4_3_intro C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S
623 n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
624 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
625 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
626 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) x3 x4 x5
627 (drop_drop (Bind Abbr) n x0 (CHead x3 (Bind Abbr) x4) H20 x1) H16 H17
628 H18))))))))))) H14)) H13)) c2 H9)))))))) H8)) H7))))) (\lambda (H5: (csuba g
629 (CHead c (Bind Void) t) c2)).(\lambda (H6: (drop (r (Bind Void) n) O c (CHead
630 d1 (Bind Abst) u1))).(let H_x \def (csuba_gen_void g c c2 t H5) in (let H7
631 \def H_x in (ex2_ind C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Void) t)))
632 (\lambda (d2: C).(csuba g c d2)) (or (ex2 C (\lambda (d2: C).(drop (S n) O c2
633 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
634 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c2 (CHead d2
635 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
636 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
637 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
638 u2 a)))))) (\lambda (x: C).(\lambda (H8: (eq C c2 (CHead x (Bind Void)
639 t))).(\lambda (H9: (csuba g c x)).(eq_ind_r C (CHead x (Bind Void) t)
640 (\lambda (c0: C).(or (ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind
641 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
642 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c0 (CHead d2 (Bind Abbr)
643 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
644 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
645 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
646 a))))))) (let H10 \def (H c d1 u1 H6 g x H9) in (or_ind (ex2 C (\lambda (d2:
647 C).(drop n O x (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
648 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O x
649 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
650 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
651 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
652 A).(arity g d2 u2 a))))) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x
653 (Bind Void) t) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
654 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O
655 (CHead x (Bind Void) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
656 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
657 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
658 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda
659 (H11: (ex2 C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abst) u1)))
660 (\lambda (d2: C).(csuba g d1 d2)))).(ex2_ind C (\lambda (d2: C).(drop n O x
661 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) (or (ex2 C
662 (\lambda (d2: C).(drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst)
663 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
664 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Void) t)
665 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
666 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
667 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
668 A).(arity g d2 u2 a)))))) (\lambda (x0: C).(\lambda (H12: (drop n O x (CHead
669 x0 (Bind Abst) u1))).(\lambda (H13: (csuba g d1 x0)).(let H14 \def
670 (refl_equal nat (r (Bind Abbr) n)) in (let H15 \def (eq_ind nat n (\lambda
671 (n0: nat).(drop n0 O x (CHead x0 (Bind Abst) u1))) H12 (r (Bind Abbr) n) H14)
672 in (or_introl (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Void) t)
673 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
674 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x
675 (Bind Void) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
676 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
677 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
678 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex_intro2 C (\lambda (d2:
679 C).(drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u1))) (\lambda
680 (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Void) n x (CHead x0 (Bind Abst)
681 u1) H15 t) H13))))))) H11)) (\lambda (H11: (ex4_3 C T A (\lambda (d2:
682 C).(\lambda (u2: T).(\lambda (_: A).(drop n O x (CHead d2 (Bind Abbr) u2)))))
683 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
684 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
685 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
686 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
687 A).(drop n O x (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
688 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
689 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
690 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) (or (ex2 C (\lambda (d2:
691 C).(drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u1))) (\lambda
692 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
693 T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind
694 Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1
695 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc
696 g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
697 a)))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H12:
698 (drop n O x (CHead x0 (Bind Abbr) x1))).(\lambda (H13: (csuba g d1
699 x0)).(\lambda (H14: (arity g d1 u1 (asucc g x2))).(\lambda (H15: (arity g x0
700 x1 x2)).(let H16 \def (refl_equal nat (r (Bind Abbr) n)) in (let H17 \def
701 (eq_ind nat n (\lambda (n0: nat).(drop n0 O x (CHead x0 (Bind Abbr) x1))) H12
702 (r (Bind Abbr) n) H16) in (or_intror (ex2 C (\lambda (d2: C).(drop (S n) O
703 (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g
704 d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop
705 (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
706 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
707 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
708 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex4_3_intro C
709 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x
710 (Bind Void) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
711 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
712 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
713 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) x0 x1 x2 (drop_drop (Bind Void)
714 n x (CHead x0 (Bind Abbr) x1) H17 t) H13 H14 H15))))))))))) H11)) H10)) c2
715 H8)))) H7))))) b H3 H4)))) (\lambda (f: F).(\lambda (H3: (csuba g (CHead c
716 (Flat f) t) c2)).(\lambda (H4: (drop (r (Flat f) n) O c (CHead d1 (Bind Abst)
717 u1))).(let H_x \def (csuba_gen_flat g c c2 t f H3) in (let H5 \def H_x in
718 (ex2_2_ind C T (\lambda (d2: C).(\lambda (u2: T).(eq C c2 (CHead d2 (Flat f)
719 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g c d2))) (or (ex2 C (\lambda
720 (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba
721 g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
722 A).(drop (S n) O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda
723 (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
724 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
725 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x0: C).(\lambda (x1:
726 T).(\lambda (H6: (eq C c2 (CHead x0 (Flat f) x1))).(\lambda (H7: (csuba g c
727 x0)).(eq_ind_r C (CHead x0 (Flat f) x1) (\lambda (c0: C).(or (ex2 C (\lambda
728 (d2: C).(drop (S n) O c0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba
729 g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
730 A).(drop (S n) O c0 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda
731 (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
732 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
733 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))))) (let H8 \def (H0 d1 u1 H4 g
734 x0 H7) in (or_ind (ex2 C (\lambda (d2: C).(drop (S n) O x0 (CHead d2 (Bind
735 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
736 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O x0 (CHead d2 (Bind Abbr)
737 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
738 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
739 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
740 a))))) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Flat f) x1)
741 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
742 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0
743 (Flat f) x1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
744 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
745 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
746 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (H9: (ex2 C (\lambda
747 (d2: C).(drop (S n) O x0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba
748 g d1 d2)))).(ex2_ind C (\lambda (d2: C).(drop (S n) O x0 (CHead d2 (Bind
749 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) (or (ex2 C (\lambda (d2:
750 C).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1))) (\lambda
751 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
752 T).(\lambda (_: A).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abbr)
753 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
754 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
755 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
756 a)))))) (\lambda (x: C).(\lambda (H10: (drop (S n) O x0 (CHead x (Bind Abst)
757 u1))).(\lambda (H11: (csuba g d1 x)).(or_introl (ex2 C (\lambda (d2: C).(drop
758 (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1))) (\lambda (d2:
759 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
760 (_: A).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abbr) u2)))))
761 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
762 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
763 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))
764 (ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2
765 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) x (drop_drop (Flat f) n
766 x0 (CHead x (Bind Abst) u1) H10 x1) H11))))) H9)) (\lambda (H9: (ex4_3 C T A
767 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O x0 (CHead d2
768 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
769 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
770 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
771 u2 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
772 A).(drop (S n) O x0 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda
773 (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
774 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
775 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) (or (ex2 C (\lambda (d2:
776 C).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1))) (\lambda
777 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
778 T).(\lambda (_: A).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abbr)
779 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
780 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
781 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
782 a)))))) (\lambda (x2: C).(\lambda (x3: T).(\lambda (x4: A).(\lambda (H10:
783 (drop (S n) O x0 (CHead x2 (Bind Abbr) x3))).(\lambda (H11: (csuba g d1
784 x2)).(\lambda (H12: (arity g d1 u1 (asucc g x4))).(\lambda (H13: (arity g x2
785 x3 x4)).(or_intror (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Flat f)
786 x1) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T
787 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0
788 (Flat f) x1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
789 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
790 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
791 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex4_3_intro C T A (\lambda
792 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0 (Flat f) x1)
793 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
794 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
795 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
796 A).(arity g d2 u2 a)))) x2 x3 x4 (drop_drop (Flat f) n x0 (CHead x2 (Bind
797 Abbr) x3) H10 x1) H11 H12 H13))))))))) H9)) H8)) c2 H6))))) H5)))))) k H2
798 (drop_gen_drop k c (CHead d1 (Bind Abst) u1) t n H1)))))))))))) c1)))) i).
800 theorem csuba_drop_abst_rev:
801 \forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).((drop i
802 O c1 (CHead d1 (Bind Abst) u)) \to (\forall (g: G).(\forall (c2: C).((csuba g
803 c2 c1) \to (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abst) u)))
804 (\lambda (d2: C).(csuba g d2 d1))))))))))
806 \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (d1:
807 C).(\forall (u: T).((drop n O c1 (CHead d1 (Bind Abst) u)) \to (\forall (g:
808 G).(\forall (c2: C).((csuba g c2 c1) \to (ex2 C (\lambda (d2: C).(drop n O c2
809 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))))))))))
810 (\lambda (c1: C).(\lambda (d1: C).(\lambda (u: T).(\lambda (H: (drop O O c1
811 (CHead d1 (Bind Abst) u))).(\lambda (g: G).(\lambda (c2: C).(\lambda (H0:
812 (csuba g c2 c1)).(let H1 \def (eq_ind C c1 (\lambda (c: C).(csuba g c2 c)) H0
813 (CHead d1 (Bind Abst) u) (drop_gen_refl c1 (CHead d1 (Bind Abst) u) H)) in
814 (let H_x \def (csuba_gen_abst_rev g d1 c2 u H1) in (let H2 \def H_x in
815 (ex2_ind C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
816 C).(csuba g d2 d1)) (ex2 C (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind
817 Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (\lambda (x: C).(\lambda (H3:
818 (eq C c2 (CHead x (Bind Abst) u))).(\lambda (H4: (csuba g x d1)).(eq_ind_r C
819 (CHead x (Bind Abst) u) (\lambda (c: C).(ex2 C (\lambda (d2: C).(drop O O c
820 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))) (ex_intro2 C
821 (\lambda (d2: C).(drop O O (CHead x (Bind Abst) u) (CHead d2 (Bind Abst) u)))
822 (\lambda (d2: C).(csuba g d2 d1)) x (drop_refl (CHead x (Bind Abst) u)) H4)
823 c2 H3)))) H2))))))))))) (\lambda (n: nat).(\lambda (H: ((\forall (c1:
824 C).(\forall (d1: C).(\forall (u: T).((drop n O c1 (CHead d1 (Bind Abst) u))
825 \to (\forall (g: G).(\forall (c2: C).((csuba g c2 c1) \to (ex2 C (\lambda
826 (d2: C).(drop n O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
827 d1)))))))))))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (d1:
828 C).(\forall (u: T).((drop (S n) O c (CHead d1 (Bind Abst) u)) \to (\forall
829 (g: G).(\forall (c2: C).((csuba g c2 c) \to (ex2 C (\lambda (d2: C).(drop (S
830 n) O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))))))))))
831 (\lambda (n0: nat).(\lambda (d1: C).(\lambda (u: T).(\lambda (H0: (drop (S n)
832 O (CSort n0) (CHead d1 (Bind Abst) u))).(\lambda (g: G).(\lambda (c2:
833 C).(\lambda (_: (csuba g c2 (CSort n0))).(and3_ind (eq C (CHead d1 (Bind
834 Abst) u) (CSort n0)) (eq nat (S n) O) (eq nat O O) (ex2 C (\lambda (d2:
835 C).(drop (S n) O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
836 d1))) (\lambda (_: (eq C (CHead d1 (Bind Abst) u) (CSort n0))).(\lambda (H3:
837 (eq nat (S n) O)).(\lambda (_: (eq nat O O)).(let H5 \def (eq_ind nat (S n)
838 (\lambda (ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O
839 \Rightarrow False | (S _) \Rightarrow True])) I O H3) in (False_ind (ex2 C
840 (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
841 C).(csuba g d2 d1))) H5))))) (drop_gen_sort n0 (S n) O (CHead d1 (Bind Abst)
842 u) H0))))))))) (\lambda (c: C).(\lambda (H0: ((\forall (d1: C).(\forall (u:
843 T).((drop (S n) O c (CHead d1 (Bind Abst) u)) \to (\forall (g: G).(\forall
844 (c2: C).((csuba g c2 c) \to (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead
845 d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))))))))))).(\lambda (k:
846 K).(\lambda (t: T).(\lambda (d1: C).(\lambda (u: T).(\lambda (H1: (drop (S n)
847 O (CHead c k t) (CHead d1 (Bind Abst) u))).(\lambda (g: G).(\lambda (c2:
848 C).(\lambda (H2: (csuba g c2 (CHead c k t))).(K_ind (\lambda (k0: K).((csuba
849 g c2 (CHead c k0 t)) \to ((drop (r k0 n) O c (CHead d1 (Bind Abst) u)) \to
850 (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u))) (\lambda
851 (d2: C).(csuba g d2 d1)))))) (\lambda (b: B).(\lambda (H3: (csuba g c2 (CHead
852 c (Bind b) t))).(\lambda (H4: (drop (r (Bind b) n) O c (CHead d1 (Bind Abst)
853 u))).(B_ind (\lambda (b0: B).((csuba g c2 (CHead c (Bind b0) t)) \to ((drop
854 (r (Bind b0) n) O c (CHead d1 (Bind Abst) u)) \to (ex2 C (\lambda (d2:
855 C).(drop (S n) O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
856 d1)))))) (\lambda (H5: (csuba g c2 (CHead c (Bind Abbr) t))).(\lambda (H6:
857 (drop (r (Bind Abbr) n) O c (CHead d1 (Bind Abst) u))).(let H_x \def
858 (csuba_gen_abbr_rev g c c2 t H5) in (let H7 \def H_x in (or_ind (ex2 C
859 (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abbr) t))) (\lambda (d2: C).(csuba
860 g d2 c))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq
861 C c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
862 (_: A).(csuba g d2 c)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
863 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
864 (a: A).(arity g c t a))))) (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2
865 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (\lambda (H8: (ex2 C
866 (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abbr) t))) (\lambda (d2: C).(csuba
867 g d2 c)))).(ex2_ind C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abbr) t)))
868 (\lambda (d2: C).(csuba g d2 c)) (ex2 C (\lambda (d2: C).(drop (S n) O c2
869 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (\lambda (x:
870 C).(\lambda (H9: (eq C c2 (CHead x (Bind Abbr) t))).(\lambda (H10: (csuba g x
871 c)).(eq_ind_r C (CHead x (Bind Abbr) t) (\lambda (c0: C).(ex2 C (\lambda (d2:
872 C).(drop (S n) O c0 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
873 d1)))) (let H11 \def (H c d1 u H6 g x H10) in (ex2_ind C (\lambda (d2:
874 C).(drop n O x (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))
875 (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind
876 Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (\lambda (x0: C).(\lambda (H12:
877 (drop n O x (CHead x0 (Bind Abst) u))).(\lambda (H13: (csuba g x0 d1)).(let
878 H14 \def (refl_equal nat (r (Bind Abst) n)) in (let H15 \def (eq_ind nat n
879 (\lambda (n0: nat).(drop n0 O x (CHead x0 (Bind Abst) u))) H12 (r (Bind Abst)
880 n) H14) in (ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abbr)
881 t) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) x0 (drop_drop
882 (Bind Abbr) n x (CHead x0 (Bind Abst) u) H15 t) H13)))))) H11)) c2 H9))))
883 H8)) (\lambda (H8: (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
884 (_: A).(eq C c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
885 T).(\lambda (_: A).(csuba g d2 c)))) (\lambda (d2: C).(\lambda (u2:
886 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
887 (_: T).(\lambda (a: A).(arity g c t a)))))).(ex4_3_ind C T A (\lambda (d2:
888 C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abst) u2)))))
889 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 c)))) (\lambda
890 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
891 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g c t a)))) (ex2 C
892 (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
893 C).(csuba g d2 d1))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2:
894 A).(\lambda (H9: (eq C c2 (CHead x0 (Bind Abst) x1))).(\lambda (H10: (csuba g
895 x0 c)).(\lambda (_: (arity g x0 x1 (asucc g x2))).(\lambda (_: (arity g c t
896 x2)).(eq_ind_r C (CHead x0 (Bind Abst) x1) (\lambda (c0: C).(ex2 C (\lambda
897 (d2: C).(drop (S n) O c0 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g
898 d2 d1)))) (let H13 \def (H c d1 u H6 g x0 H10) in (ex2_ind C (\lambda (d2:
899 C).(drop n O x0 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))
900 (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2
901 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (\lambda (x: C).(\lambda
902 (H14: (drop n O x0 (CHead x (Bind Abst) u))).(\lambda (H15: (csuba g x
903 d1)).(let H16 \def (refl_equal nat (r (Bind Abst) n)) in (let H17 \def
904 (eq_ind nat n (\lambda (n0: nat).(drop n0 O x0 (CHead x (Bind Abst) u))) H14
905 (r (Bind Abst) n) H16) in (ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead
906 x0 (Bind Abst) x1) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
907 d1)) x (drop_drop (Bind Abst) n x0 (CHead x (Bind Abst) u) H17 x1) H15))))))
908 H13)) c2 H9)))))))) H8)) H7))))) (\lambda (H5: (csuba g c2 (CHead c (Bind
909 Abst) t))).(\lambda (H6: (drop (r (Bind Abst) n) O c (CHead d1 (Bind Abst)
910 u))).(let H_x \def (csuba_gen_abst_rev g c c2 t H5) in (let H7 \def H_x in
911 (ex2_ind C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) t))) (\lambda (d2:
912 C).(csuba g d2 c)) (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind
913 Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (\lambda (x: C).(\lambda (H8:
914 (eq C c2 (CHead x (Bind Abst) t))).(\lambda (H9: (csuba g x c)).(eq_ind_r C
915 (CHead x (Bind Abst) t) (\lambda (c0: C).(ex2 C (\lambda (d2: C).(drop (S n)
916 O c0 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))) (let H10
917 \def (H c d1 u H6 g x H9) in (ex2_ind C (\lambda (d2: C).(drop n O x (CHead
918 d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) (ex2 C (\lambda (d2:
919 C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u))) (\lambda
920 (d2: C).(csuba g d2 d1))) (\lambda (x0: C).(\lambda (H11: (drop n O x (CHead
921 x0 (Bind Abst) u))).(\lambda (H12: (csuba g x0 d1)).(let H13 \def (refl_equal
922 nat (r (Bind Abst) n)) in (let H14 \def (eq_ind nat n (\lambda (n0:
923 nat).(drop n0 O x (CHead x0 (Bind Abst) u))) H11 (r (Bind Abst) n) H13) in
924 (ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2
925 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) x0 (drop_drop (Bind Abst)
926 n x (CHead x0 (Bind Abst) u) H14 t) H12)))))) H10)) c2 H8)))) H7)))))
927 (\lambda (H5: (csuba g c2 (CHead c (Bind Void) t))).(\lambda (H6: (drop (r
928 (Bind Void) n) O c (CHead d1 (Bind Abst) u))).(let H_x \def
929 (csuba_gen_void_rev g c c2 t H5) in (let H7 \def H_x in (ex2_ind C (\lambda
930 (d2: C).(eq C c2 (CHead d2 (Bind Void) t))) (\lambda (d2: C).(csuba g d2 c))
931 (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u))) (\lambda
932 (d2: C).(csuba g d2 d1))) (\lambda (x: C).(\lambda (H8: (eq C c2 (CHead x
933 (Bind Void) t))).(\lambda (H9: (csuba g x c)).(eq_ind_r C (CHead x (Bind
934 Void) t) (\lambda (c0: C).(ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2
935 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))) (let H10 \def (H c d1 u
936 H6 g x H9) in (ex2_ind C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abst)
937 u))) (\lambda (d2: C).(csuba g d2 d1)) (ex2 C (\lambda (d2: C).(drop (S n) O
938 (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g
939 d2 d1))) (\lambda (x0: C).(\lambda (H11: (drop n O x (CHead x0 (Bind Abst)
940 u))).(\lambda (H12: (csuba g x0 d1)).(let H13 \def (refl_equal nat (r (Bind
941 Abst) n)) in (let H14 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O x
942 (CHead x0 (Bind Abst) u))) H11 (r (Bind Abst) n) H13) in (ex_intro2 C
943 (\lambda (d2: C).(drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst)
944 u))) (\lambda (d2: C).(csuba g d2 d1)) x0 (drop_drop (Bind Void) n x (CHead
945 x0 (Bind Abst) u) H14 t) H12)))))) H10)) c2 H8)))) H7))))) b H3 H4))))
946 (\lambda (f: F).(\lambda (H3: (csuba g c2 (CHead c (Flat f) t))).(\lambda
947 (H4: (drop (r (Flat f) n) O c (CHead d1 (Bind Abst) u))).(let H_x \def
948 (csuba_gen_flat_rev g c c2 t f H3) in (let H5 \def H_x in (ex2_2_ind C T
949 (\lambda (d2: C).(\lambda (u2: T).(eq C c2 (CHead d2 (Flat f) u2)))) (\lambda
950 (d2: C).(\lambda (_: T).(csuba g d2 c))) (ex2 C (\lambda (d2: C).(drop (S n)
951 O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (\lambda
952 (x0: C).(\lambda (x1: T).(\lambda (H6: (eq C c2 (CHead x0 (Flat f)
953 x1))).(\lambda (H7: (csuba g x0 c)).(eq_ind_r C (CHead x0 (Flat f) x1)
954 (\lambda (c0: C).(ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind
955 Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))) (let H8 \def (H0 d1 u H4 g x0
956 H7) in (ex2_ind C (\lambda (d2: C).(drop (S n) O x0 (CHead d2 (Bind Abst)
957 u))) (\lambda (d2: C).(csuba g d2 d1)) (ex2 C (\lambda (d2: C).(drop (S n) O
958 (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g
959 d2 d1))) (\lambda (x: C).(\lambda (H9: (drop (S n) O x0 (CHead x (Bind Abst)
960 u))).(\lambda (H10: (csuba g x d1)).(ex_intro2 C (\lambda (d2: C).(drop (S n)
961 O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g
962 d2 d1)) x (drop_drop (Flat f) n x0 (CHead x (Bind Abst) u) H9 x1) H10))))
963 H8)) c2 H6))))) H5)))))) k H2 (drop_gen_drop k c (CHead d1 (Bind Abst) u) t n
964 H1)))))))))))) c1)))) i).
966 theorem csuba_drop_abbr_rev:
967 \forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).((drop i
968 O c1 (CHead d1 (Bind Abbr) u1)) \to (\forall (g: G).(\forall (c2: C).((csuba
969 g c2 c1) \to (or (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abbr)
970 u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
971 C).(\lambda (u2: T).(\lambda (_: A).(drop i O c2 (CHead d2 (Bind Abst)
972 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
973 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
974 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
977 \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (d1:
978 C).(\forall (u1: T).((drop n O c1 (CHead d1 (Bind Abbr) u1)) \to (\forall (g:
979 G).(\forall (c2: C).((csuba g c2 c1) \to (or (ex2 C (\lambda (d2: C).(drop n
980 O c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C
981 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O c2 (CHead d2
982 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
983 d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
984 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
985 u1 a)))))))))))))) (\lambda (c1: C).(\lambda (d1: C).(\lambda (u1:
986 T).(\lambda (H: (drop O O c1 (CHead d1 (Bind Abbr) u1))).(\lambda (g:
987 G).(\lambda (c2: C).(\lambda (H0: (csuba g c2 c1)).(let H1 \def (eq_ind C c1
988 (\lambda (c: C).(csuba g c2 c)) H0 (CHead d1 (Bind Abbr) u1) (drop_gen_refl
989 c1 (CHead d1 (Bind Abbr) u1) H)) in (let H_x \def (csuba_gen_abbr_rev g d1 c2
990 u1 H1) in (let H2 \def H_x in (or_ind (ex2 C (\lambda (d2: C).(eq C c2 (CHead
991 d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
992 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abst)
993 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
994 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
995 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
996 (or (ex2 C (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abbr) u1))) (\lambda
997 (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
998 T).(\lambda (_: A).(drop O O c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
999 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
1000 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
1001 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))) (\lambda (H3:
1002 (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
1003 C).(csuba g d2 d1)))).(ex2_ind C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind
1004 Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)) (or (ex2 C (\lambda (d2:
1005 C).(drop O O c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
1006 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O
1007 O c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
1008 (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1009 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1010 (a: A).(arity g d1 u1 a)))))) (\lambda (x: C).(\lambda (H4: (eq C c2 (CHead x
1011 (Bind Abbr) u1))).(\lambda (H5: (csuba g x d1)).(eq_ind_r C (CHead x (Bind
1012 Abbr) u1) (\lambda (c: C).(or (ex2 C (\lambda (d2: C).(drop O O c (CHead d2
1013 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
1014 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O c (CHead d2 (Bind Abst)
1015 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
1016 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
1017 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
1018 a))))))) (or_introl (ex2 C (\lambda (d2: C).(drop O O (CHead x (Bind Abbr)
1019 u1) (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T
1020 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O (CHead x (Bind
1021 Abbr) u1) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
1022 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1023 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1024 (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex_intro2 C (\lambda (d2:
1025 C).(drop O O (CHead x (Bind Abbr) u1) (CHead d2 (Bind Abbr) u1))) (\lambda
1026 (d2: C).(csuba g d2 d1)) x (drop_refl (CHead x (Bind Abbr) u1)) H5)) c2
1027 H4)))) H3)) (\lambda (H3: (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
1028 T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
1029 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
1030 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
1031 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))).(ex4_3_ind C T
1032 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind
1033 Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2
1034 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
1035 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
1036 u1 a)))) (or (ex2 C (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abbr) u1)))
1037 (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda
1038 (u2: T).(\lambda (_: A).(drop O O c2 (CHead d2 (Bind Abst) u2))))) (\lambda
1039 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
1040 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
1041 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))) (\lambda (x0:
1042 C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H4: (eq C c2 (CHead x0 (Bind
1043 Abst) x1))).(\lambda (H5: (csuba g x0 d1)).(\lambda (H6: (arity g x0 x1
1044 (asucc g x2))).(\lambda (H7: (arity g d1 u1 x2)).(eq_ind_r C (CHead x0 (Bind
1045 Abst) x1) (\lambda (c: C).(or (ex2 C (\lambda (d2: C).(drop O O c (CHead d2
1046 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
1047 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O c (CHead d2 (Bind Abst)
1048 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
1049 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
1050 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
1051 a))))))) (or_intror (ex2 C (\lambda (d2: C).(drop O O (CHead x0 (Bind Abst)
1052 x1) (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T
1053 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O (CHead x0 (Bind
1054 Abst) x1) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
1055 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1056 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1057 (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex4_3_intro C T A (\lambda (d2:
1058 C).(\lambda (u2: T).(\lambda (_: A).(drop O O (CHead x0 (Bind Abst) x1)
1059 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
1060 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1061 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1062 (a: A).(arity g d1 u1 a)))) x0 x1 x2 (drop_refl (CHead x0 (Bind Abst) x1)) H5
1063 H6 H7)) c2 H4)))))))) H3)) H2))))))))))) (\lambda (n: nat).(\lambda (H:
1064 ((\forall (c1: C).(\forall (d1: C).(\forall (u1: T).((drop n O c1 (CHead d1
1065 (Bind Abbr) u1)) \to (\forall (g: G).(\forall (c2: C).((csuba g c2 c1) \to
1066 (or (ex2 C (\lambda (d2: C).(drop n O c2 (CHead d2 (Bind Abbr) u1))) (\lambda
1067 (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
1068 T).(\lambda (_: A).(drop n O c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
1069 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
1070 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
1071 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
1072 a))))))))))))))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (d1:
1073 C).(\forall (u1: T).((drop (S n) O c (CHead d1 (Bind Abbr) u1)) \to (\forall
1074 (g: G).(\forall (c2: C).((csuba g c2 c) \to (or (ex2 C (\lambda (d2: C).(drop
1075 (S n) O c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))
1076 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O
1077 c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
1078 (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1079 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1080 (a: A).(arity g d1 u1 a))))))))))))) (\lambda (n0: nat).(\lambda (d1:
1081 C).(\lambda (u1: T).(\lambda (H0: (drop (S n) O (CSort n0) (CHead d1 (Bind
1082 Abbr) u1))).(\lambda (g: G).(\lambda (c2: C).(\lambda (_: (csuba g c2 (CSort
1083 n0))).(and3_ind (eq C (CHead d1 (Bind Abbr) u1) (CSort n0)) (eq nat (S n) O)
1084 (eq nat O O) (or (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind
1085 Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
1086 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c2 (CHead d2 (Bind Abst)
1087 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
1088 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
1089 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))))
1090 (\lambda (_: (eq C (CHead d1 (Bind Abbr) u1) (CSort n0))).(\lambda (H3: (eq
1091 nat (S n) O)).(\lambda (_: (eq nat O O)).(let H5 \def (eq_ind nat (S n)
1092 (\lambda (ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O
1093 \Rightarrow False | (S _) \Rightarrow True])) I O H3) in (False_ind (or (ex2
1094 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
1095 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
1096 (_: A).(drop (S n) O c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
1097 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
1098 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
1099 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))) H5)))))
1100 (drop_gen_sort n0 (S n) O (CHead d1 (Bind Abbr) u1) H0))))))))) (\lambda (c:
1101 C).(\lambda (H0: ((\forall (d1: C).(\forall (u1: T).((drop (S n) O c (CHead
1102 d1 (Bind Abbr) u1)) \to (\forall (g: G).(\forall (c2: C).((csuba g c2 c) \to
1103 (or (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u1)))
1104 (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda
1105 (u2: T).(\lambda (_: A).(drop (S n) O c2 (CHead d2 (Bind Abst) u2)))))
1106 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
1107 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
1108 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
1109 a)))))))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (d1: C).(\lambda
1110 (u1: T).(\lambda (H1: (drop (S n) O (CHead c k t) (CHead d1 (Bind Abbr)
1111 u1))).(\lambda (g: G).(\lambda (c2: C).(\lambda (H2: (csuba g c2 (CHead c k
1112 t))).(K_ind (\lambda (k0: K).((csuba g c2 (CHead c k0 t)) \to ((drop (r k0 n)
1113 O c (CHead d1 (Bind Abbr) u1)) \to (or (ex2 C (\lambda (d2: C).(drop (S n) O
1114 c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T
1115 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c2 (CHead
1116 d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
1117 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1118 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1119 (a: A).(arity g d1 u1 a))))))))) (\lambda (b: B).(\lambda (H3: (csuba g c2
1120 (CHead c (Bind b) t))).(\lambda (H4: (drop (r (Bind b) n) O c (CHead d1 (Bind
1121 Abbr) u1))).(B_ind (\lambda (b0: B).((csuba g c2 (CHead c (Bind b0) t)) \to
1122 ((drop (r (Bind b0) n) O c (CHead d1 (Bind Abbr) u1)) \to (or (ex2 C (\lambda
1123 (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba
1124 g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
1125 A).(drop (S n) O c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda
1126 (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1127 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1128 (_: T).(\lambda (a: A).(arity g d1 u1 a))))))))) (\lambda (H5: (csuba g c2
1129 (CHead c (Bind Abbr) t))).(\lambda (H6: (drop (r (Bind Abbr) n) O c (CHead d1
1130 (Bind Abbr) u1))).(let H_x \def (csuba_gen_abbr_rev g c c2 t H5) in (let H7
1131 \def H_x in (or_ind (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abbr)
1132 t))) (\lambda (d2: C).(csuba g d2 c))) (ex4_3 C T A (\lambda (d2: C).(\lambda
1133 (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
1134 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 c)))) (\lambda (d2:
1135 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
1136 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g c t a))))) (or (ex2 C
1137 (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
1138 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
1139 (_: A).(drop (S n) O c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
1140 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
1141 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
1142 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))) (\lambda (H8:
1143 (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abbr) t))) (\lambda (d2:
1144 C).(csuba g d2 c)))).(ex2_ind C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind
1145 Abbr) t))) (\lambda (d2: C).(csuba g d2 c)) (or (ex2 C (\lambda (d2: C).(drop
1146 (S n) O c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))
1147 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O
1148 c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
1149 (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1150 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1151 (a: A).(arity g d1 u1 a)))))) (\lambda (x: C).(\lambda (H9: (eq C c2 (CHead x
1152 (Bind Abbr) t))).(\lambda (H10: (csuba g x c)).(eq_ind_r C (CHead x (Bind
1153 Abbr) t) (\lambda (c0: C).(or (ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead
1154 d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
1155 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c0 (CHead d2 (Bind
1156 Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2
1157 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
1158 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
1159 u1 a))))))) (let H11 \def (H c d1 u1 H6 g x H10) in (or_ind (ex2 C (\lambda
1160 (d2: C).(drop n O x (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
1161 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n
1162 O x (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
1163 (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1164 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1165 (a: A).(arity g d1 u1 a))))) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead
1166 x (Bind Abbr) t) (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
1167 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S
1168 n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
1169 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
1170 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
1171 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))) (\lambda (H12:
1172 (ex2 C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
1173 C).(csuba g d2 d1)))).(ex2_ind C (\lambda (d2: C).(drop n O x (CHead d2 (Bind
1174 Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)) (or (ex2 C (\lambda (d2:
1175 C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abbr) u1))) (\lambda
1176 (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
1177 T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind
1178 Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2
1179 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
1180 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
1181 u1 a)))))) (\lambda (x0: C).(\lambda (H13: (drop n O x (CHead x0 (Bind Abbr)
1182 u1))).(\lambda (H14: (csuba g x0 d1)).(let H15 \def (refl_equal nat (r (Bind
1183 Abst) n)) in (let H16 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O x
1184 (CHead x0 (Bind Abbr) u1))) H13 (r (Bind Abst) n) H15) in (or_introl (ex2 C
1185 (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abbr)
1186 u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
1187 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Abbr) t)
1188 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
1189 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1190 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1191 (a: A).(arity g d1 u1 a))))) (ex_intro2 C (\lambda (d2: C).(drop (S n) O
1192 (CHead x (Bind Abbr) t) (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g
1193 d2 d1)) x0 (drop_drop (Bind Abbr) n x (CHead x0 (Bind Abbr) u1) H16 t)
1194 H14))))))) H12)) (\lambda (H12: (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
1195 T).(\lambda (_: A).(drop n O x (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
1196 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
1197 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
1198 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))).(ex4_3_ind C T
1199 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O x (CHead d2
1200 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
1201 d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
1202 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
1203 u1 a)))) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abbr) t)
1204 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A
1205 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x
1206 (Bind Abbr) t) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
1207 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1208 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1209 (_: T).(\lambda (a: A).(arity g d1 u1 a)))))) (\lambda (x0: C).(\lambda (x1:
1210 T).(\lambda (x2: A).(\lambda (H13: (drop n O x (CHead x0 (Bind Abst)
1211 x1))).(\lambda (H14: (csuba g x0 d1)).(\lambda (H15: (arity g x0 x1 (asucc g
1212 x2))).(\lambda (H16: (arity g d1 u1 x2)).(let H17 \def (refl_equal nat (r
1213 (Bind Abst) n)) in (let H18 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O
1214 x (CHead x0 (Bind Abst) x1))) H13 (r (Bind Abst) n) H17) in (or_intror (ex2 C
1215 (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abbr)
1216 u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
1217 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Abbr) t)
1218 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
1219 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1220 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1221 (a: A).(arity g d1 u1 a))))) (ex4_3_intro C T A (\lambda (d2: C).(\lambda
1222 (u2: T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind
1223 Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2
1224 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
1225 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
1226 u1 a)))) x0 x1 x2 (drop_drop (Bind Abbr) n x (CHead x0 (Bind Abst) x1) H18 t)
1227 H14 H15 H16))))))))))) H12)) H11)) c2 H9)))) H8)) (\lambda (H8: (ex4_3 C T A
1228 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind
1229 Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2
1230 c)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc
1231 g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g c t
1232 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
1233 A).(eq C c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
1234 T).(\lambda (_: A).(csuba g d2 c)))) (\lambda (d2: C).(\lambda (u2:
1235 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1236 (_: T).(\lambda (a: A).(arity g c t a)))) (or (ex2 C (\lambda (d2: C).(drop
1237 (S n) O c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))
1238 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O
1239 c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
1240 (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1241 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1242 (a: A).(arity g d1 u1 a)))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2:
1243 A).(\lambda (H9: (eq C c2 (CHead x0 (Bind Abst) x1))).(\lambda (H10: (csuba g
1244 x0 c)).(\lambda (_: (arity g x0 x1 (asucc g x2))).(\lambda (_: (arity g c t
1245 x2)).(eq_ind_r C (CHead x0 (Bind Abst) x1) (\lambda (c0: C).(or (ex2 C
1246 (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
1247 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
1248 (_: A).(drop (S n) O c0 (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
1249 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
1250 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
1251 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))))) (let H13 \def
1252 (H c d1 u1 H6 g x0 H10) in (or_ind (ex2 C (\lambda (d2: C).(drop n O x0
1253 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A
1254 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O x0 (CHead d2
1255 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
1256 d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
1257 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
1258 u1 a))))) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Bind Abst) x1)
1259 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A
1260 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0
1261 (Bind Abst) x1) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
1262 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1263 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1264 (_: T).(\lambda (a: A).(arity g d1 u1 a)))))) (\lambda (H14: (ex2 C (\lambda
1265 (d2: C).(drop n O x0 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
1266 d1)))).(ex2_ind C (\lambda (d2: C).(drop n O x0 (CHead d2 (Bind Abbr) u1)))
1267 (\lambda (d2: C).(csuba g d2 d1)) (or (ex2 C (\lambda (d2: C).(drop (S n) O
1268 (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba
1269 g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
1270 A).(drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Abst) u2)))))
1271 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
1272 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
1273 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))))
1274 (\lambda (x: C).(\lambda (H15: (drop n O x0 (CHead x (Bind Abbr)
1275 u1))).(\lambda (H16: (csuba g x d1)).(let H17 \def (refl_equal nat (r (Bind
1276 Abst) n)) in (let H18 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O x0
1277 (CHead x (Bind Abbr) u1))) H15 (r (Bind Abst) n) H17) in (or_introl (ex2 C
1278 (\lambda (d2: C).(drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind
1279 Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
1280 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0 (Bind Abst) x1)
1281 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
1282 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1283 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1284 (a: A).(arity g d1 u1 a))))) (ex_intro2 C (\lambda (d2: C).(drop (S n) O
1285 (CHead x0 (Bind Abst) x1) (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba
1286 g d2 d1)) x (drop_drop (Bind Abst) n x0 (CHead x (Bind Abbr) u1) H18 x1)
1287 H16))))))) H14)) (\lambda (H14: (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
1288 T).(\lambda (_: A).(drop n O x0 (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
1289 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
1290 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
1291 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))).(ex4_3_ind C T
1292 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O x0 (CHead d2
1293 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
1294 d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
1295 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
1296 u1 a)))) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Bind Abst) x1)
1297 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A
1298 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0
1299 (Bind Abst) x1) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
1300 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1301 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1302 (_: T).(\lambda (a: A).(arity g d1 u1 a)))))) (\lambda (x3: C).(\lambda (x4:
1303 T).(\lambda (x5: A).(\lambda (H15: (drop n O x0 (CHead x3 (Bind Abst)
1304 x4))).(\lambda (H16: (csuba g x3 d1)).(\lambda (H17: (arity g x3 x4 (asucc g
1305 x5))).(\lambda (H18: (arity g d1 u1 x5)).(let H19 \def (refl_equal nat (r
1306 (Bind Abst) n)) in (let H20 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O
1307 x0 (CHead x3 (Bind Abst) x4))) H15 (r (Bind Abst) n) H19) in (or_intror (ex2
1308 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2 (Bind
1309 Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
1310 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0 (Bind Abst) x1)
1311 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
1312 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1313 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1314 (a: A).(arity g d1 u1 a))))) (ex4_3_intro C T A (\lambda (d2: C).(\lambda
1315 (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0 (Bind Abst) x1) (CHead d2
1316 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
1317 d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
1318 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
1319 u1 a)))) x3 x4 x5 (drop_drop (Bind Abst) n x0 (CHead x3 (Bind Abst) x4) H20
1320 x1) H16 H17 H18))))))))))) H14)) H13)) c2 H9)))))))) H8)) H7))))) (\lambda
1321 (H5: (csuba g c2 (CHead c (Bind Abst) t))).(\lambda (H6: (drop (r (Bind Abst)
1322 n) O c (CHead d1 (Bind Abbr) u1))).(let H_x \def (csuba_gen_abst_rev g c c2 t
1323 H5) in (let H7 \def H_x in (ex2_ind C (\lambda (d2: C).(eq C c2 (CHead d2
1324 (Bind Abst) t))) (\lambda (d2: C).(csuba g d2 c)) (or (ex2 C (\lambda (d2:
1325 C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
1326 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S
1327 n) O c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
1328 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1329 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1330 (_: T).(\lambda (a: A).(arity g d1 u1 a)))))) (\lambda (x: C).(\lambda (H8:
1331 (eq C c2 (CHead x (Bind Abst) t))).(\lambda (H9: (csuba g x c)).(eq_ind_r C
1332 (CHead x (Bind Abst) t) (\lambda (c0: C).(or (ex2 C (\lambda (d2: C).(drop (S
1333 n) O c0 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3
1334 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c0
1335 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
1336 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1337 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1338 (a: A).(arity g d1 u1 a))))))) (let H10 \def (H c d1 u1 H6 g x H9) in (or_ind
1339 (ex2 C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
1340 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
1341 (_: A).(drop n O x (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda
1342 (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1343 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1344 (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (or (ex2 C (\lambda (d2:
1345 C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abbr) u1))) (\lambda
1346 (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
1347 T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind
1348 Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2
1349 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
1350 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
1351 u1 a)))))) (\lambda (H11: (ex2 C (\lambda (d2: C).(drop n O x (CHead d2 (Bind
1352 Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))).(ex2_ind C (\lambda (d2:
1353 C).(drop n O x (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))
1354 (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2
1355 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
1356 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Abst)
1357 t) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
1358 (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1359 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1360 (a: A).(arity g d1 u1 a)))))) (\lambda (x0: C).(\lambda (H12: (drop n O x
1361 (CHead x0 (Bind Abbr) u1))).(\lambda (H13: (csuba g x0 d1)).(let H14 \def
1362 (refl_equal nat (r (Bind Abst) n)) in (let H15 \def (eq_ind nat n (\lambda
1363 (n0: nat).(drop n0 O x (CHead x0 (Bind Abbr) u1))) H12 (r (Bind Abst) n) H14)
1364 in (or_introl (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abst) t)
1365 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A
1366 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x
1367 (Bind Abst) t) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
1368 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1369 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1370 (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex_intro2 C (\lambda (d2:
1371 C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abbr) u1))) (\lambda
1372 (d2: C).(csuba g d2 d1)) x0 (drop_drop (Bind Abst) n x (CHead x0 (Bind Abbr)
1373 u1) H15 t) H13))))))) H11)) (\lambda (H11: (ex4_3 C T A (\lambda (d2:
1374 C).(\lambda (u2: T).(\lambda (_: A).(drop n O x (CHead d2 (Bind Abst) u2)))))
1375 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
1376 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
1377 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
1378 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
1379 A).(drop n O x (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
1380 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1381 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1382 (_: T).(\lambda (a: A).(arity g d1 u1 a)))) (or (ex2 C (\lambda (d2: C).(drop
1383 (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
1384 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
1385 (_: A).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u2)))))
1386 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
1387 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
1388 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))))
1389 (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H12: (drop n O x
1390 (CHead x0 (Bind Abst) x1))).(\lambda (H13: (csuba g x0 d1)).(\lambda (H14:
1391 (arity g x0 x1 (asucc g x2))).(\lambda (H15: (arity g d1 u1 x2)).(let H16
1392 \def (refl_equal nat (r (Bind Abst) n)) in (let H17 \def (eq_ind nat n
1393 (\lambda (n0: nat).(drop n0 O x (CHead x0 (Bind Abst) x1))) H12 (r (Bind
1394 Abst) n) H16) in (or_intror (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x
1395 (Bind Abst) t) (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))
1396 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O
1397 (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
1398 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
1399 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
1400 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex4_3_intro C T
1401 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x
1402 (Bind Abst) t) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
1403 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1404 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1405 (_: T).(\lambda (a: A).(arity g d1 u1 a)))) x0 x1 x2 (drop_drop (Bind Abst) n
1406 x (CHead x0 (Bind Abst) x1) H17 t) H13 H14 H15))))))))))) H11)) H10)) c2
1407 H8)))) H7))))) (\lambda (H5: (csuba g c2 (CHead c (Bind Void) t))).(\lambda
1408 (H6: (drop (r (Bind Void) n) O c (CHead d1 (Bind Abbr) u1))).(let H_x \def
1409 (csuba_gen_void_rev g c c2 t H5) in (let H7 \def H_x in (ex2_ind C (\lambda
1410 (d2: C).(eq C c2 (CHead d2 (Bind Void) t))) (\lambda (d2: C).(csuba g d2 c))
1411 (or (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u1)))
1412 (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda
1413 (u2: T).(\lambda (_: A).(drop (S n) O c2 (CHead d2 (Bind Abst) u2)))))
1414 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
1415 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
1416 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))))
1417 (\lambda (x: C).(\lambda (H8: (eq C c2 (CHead x (Bind Void) t))).(\lambda
1418 (H9: (csuba g x c)).(eq_ind_r C (CHead x (Bind Void) t) (\lambda (c0: C).(or
1419 (ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind Abbr) u1))) (\lambda
1420 (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
1421 T).(\lambda (_: A).(drop (S n) O c0 (CHead d2 (Bind Abst) u2))))) (\lambda
1422 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
1423 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
1424 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))))) (let H10 \def
1425 (H c d1 u1 H6 g x H9) in (or_ind (ex2 C (\lambda (d2: C).(drop n O x (CHead
1426 d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
1427 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O x (CHead d2 (Bind Abst)
1428 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
1429 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
1430 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
1431 (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Void) t) (CHead d2
1432 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
1433 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Void)
1434 t) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
1435 (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1436 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1437 (a: A).(arity g d1 u1 a)))))) (\lambda (H11: (ex2 C (\lambda (d2: C).(drop n
1438 O x (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))).(ex2_ind
1439 C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
1440 C).(csuba g d2 d1)) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind
1441 Void) t) (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))
1442 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O
1443 (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
1444 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
1445 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
1446 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))) (\lambda (x0:
1447 C).(\lambda (H12: (drop n O x (CHead x0 (Bind Abbr) u1))).(\lambda (H13:
1448 (csuba g x0 d1)).(let H14 \def (refl_equal nat (r (Bind Abst) n)) in (let H15
1449 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O x (CHead x0 (Bind Abbr)
1450 u1))) H12 (r (Bind Abst) n) H14) in (or_introl (ex2 C (\lambda (d2: C).(drop
1451 (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
1452 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
1453 (_: A).(drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u2)))))
1454 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
1455 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
1456 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
1457 (ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Void) t) (CHead d2
1458 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)) x0 (drop_drop (Bind Void)
1459 n x (CHead x0 (Bind Abbr) u1) H15 t) H13))))))) H11)) (\lambda (H11: (ex4_3 C
1460 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O x (CHead d2
1461 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
1462 d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
1463 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
1464 u1 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
1465 A).(drop n O x (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
1466 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1467 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1468 (_: T).(\lambda (a: A).(arity g d1 u1 a)))) (or (ex2 C (\lambda (d2: C).(drop
1469 (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
1470 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
1471 (_: A).(drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u2)))))
1472 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
1473 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
1474 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))))
1475 (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H12: (drop n O x
1476 (CHead x0 (Bind Abst) x1))).(\lambda (H13: (csuba g x0 d1)).(\lambda (H14:
1477 (arity g x0 x1 (asucc g x2))).(\lambda (H15: (arity g d1 u1 x2)).(let H16
1478 \def (refl_equal nat (r (Bind Abst) n)) in (let H17 \def (eq_ind nat n
1479 (\lambda (n0: nat).(drop n0 O x (CHead x0 (Bind Abst) x1))) H12 (r (Bind
1480 Abst) n) H16) in (or_intror (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x
1481 (Bind Void) t) (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))
1482 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O
1483 (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
1484 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
1485 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
1486 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex4_3_intro C T
1487 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x
1488 (Bind Void) t) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
1489 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1490 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1491 (_: T).(\lambda (a: A).(arity g d1 u1 a)))) x0 x1 x2 (drop_drop (Bind Void) n
1492 x (CHead x0 (Bind Abst) x1) H17 t) H13 H14 H15))))))))))) H11)) H10)) c2
1493 H8)))) H7))))) b H3 H4)))) (\lambda (f: F).(\lambda (H3: (csuba g c2 (CHead c
1494 (Flat f) t))).(\lambda (H4: (drop (r (Flat f) n) O c (CHead d1 (Bind Abbr)
1495 u1))).(let H_x \def (csuba_gen_flat_rev g c c2 t f H3) in (let H5 \def H_x in
1496 (ex2_2_ind C T (\lambda (d2: C).(\lambda (u2: T).(eq C c2 (CHead d2 (Flat f)
1497 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 c))) (or (ex2 C (\lambda
1498 (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba
1499 g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
1500 A).(drop (S n) O c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda
1501 (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1502 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1503 (_: T).(\lambda (a: A).(arity g d1 u1 a)))))) (\lambda (x0: C).(\lambda (x1:
1504 T).(\lambda (H6: (eq C c2 (CHead x0 (Flat f) x1))).(\lambda (H7: (csuba g x0
1505 c)).(eq_ind_r C (CHead x0 (Flat f) x1) (\lambda (c0: C).(or (ex2 C (\lambda
1506 (d2: C).(drop (S n) O c0 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba
1507 g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
1508 A).(drop (S n) O c0 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda
1509 (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1510 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1511 (_: T).(\lambda (a: A).(arity g d1 u1 a))))))) (let H8 \def (H0 d1 u1 H4 g x0
1512 H7) in (or_ind (ex2 C (\lambda (d2: C).(drop (S n) O x0 (CHead d2 (Bind Abbr)
1513 u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
1514 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O x0 (CHead d2 (Bind Abst)
1515 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
1516 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
1517 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
1518 (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2
1519 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
1520 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0 (Flat f) x1)
1521 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
1522 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1523 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1524 (a: A).(arity g d1 u1 a)))))) (\lambda (H9: (ex2 C (\lambda (d2: C).(drop (S
1525 n) O x0 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
1526 d1)))).(ex2_ind C (\lambda (d2: C).(drop (S n) O x0 (CHead d2 (Bind Abbr)
1527 u1))) (\lambda (d2: C).(csuba g d2 d1)) (or (ex2 C (\lambda (d2: C).(drop (S
1528 n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
1529 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
1530 (_: A).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u2)))))
1531 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
1532 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
1533 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))))
1534 (\lambda (x: C).(\lambda (H10: (drop (S n) O x0 (CHead x (Bind Abbr)
1535 u1))).(\lambda (H11: (csuba g x d1)).(or_introl (ex2 C (\lambda (d2: C).(drop
1536 (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
1537 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
1538 (_: A).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u2)))))
1539 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
1540 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
1541 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
1542 (ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2
1543 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)) x (drop_drop (Flat f) n
1544 x0 (CHead x (Bind Abbr) u1) H10 x1) H11))))) H9)) (\lambda (H9: (ex4_3 C T A
1545 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O x0 (CHead d2
1546 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
1547 d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
1548 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
1549 u1 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
1550 A).(drop (S n) O x0 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda
1551 (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1552 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1553 (_: T).(\lambda (a: A).(arity g d1 u1 a)))) (or (ex2 C (\lambda (d2: C).(drop
1554 (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
1555 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
1556 (_: A).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u2)))))
1557 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
1558 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
1559 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))))
1560 (\lambda (x2: C).(\lambda (x3: T).(\lambda (x4: A).(\lambda (H10: (drop (S n)
1561 O x0 (CHead x2 (Bind Abst) x3))).(\lambda (H11: (csuba g x2 d1)).(\lambda
1562 (H12: (arity g x2 x3 (asucc g x4))).(\lambda (H13: (arity g d1 u1
1563 x4)).(or_intror (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Flat f) x1)
1564 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A
1565 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0
1566 (Flat f) x1) (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
1567 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1568 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1569 (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex4_3_intro C T A (\lambda (d2:
1570 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0 (Flat f) x1)
1571 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
1572 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1573 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1574 (a: A).(arity g d1 u1 a)))) x2 x3 x4 (drop_drop (Flat f) n x0 (CHead x2 (Bind
1575 Abst) x3) H10 x1) H11 H12 H13))))))))) H9)) H8)) c2 H6))))) H5)))))) k H2
1576 (drop_gen_drop k c (CHead d1 (Bind Abbr) u1) t n H1)))))))))))) c1)))) i).
projects / helm.git / blob