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