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