1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/drop".
19 include "csuba/fwd.ma".
21 include "drop/fwd.ma".
23 theorem csuba_drop_abbr:
24 \forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).((drop i
25 O c1 (CHead d1 (Bind Abbr) u)) \to (\forall (g: G).(\forall (c2: C).((csuba g
26 c1 c2) \to (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abbr) u)))
27 (\lambda (d2: C).(csuba g d1 d2))))))))))
29 \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (d1:
30 C).(\forall (u: T).((drop n O c1 (CHead d1 (Bind Abbr) u)) \to (\forall (g:
31 G).(\forall (c2: C).((csuba g c1 c2) \to (ex2 C (\lambda (d2: C).(drop n O c2
32 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))))))))))
33 (\lambda (c1: C).(\lambda (d1: C).(\lambda (u: T).(\lambda (H: (drop O O c1
34 (CHead d1 (Bind Abbr) u))).(\lambda (g: G).(\lambda (c2: C).(\lambda (H0:
35 (csuba g c1 c2)).(let H1 \def (eq_ind C c1 (\lambda (c: C).(csuba g c c2)) H0
36 (CHead d1 (Bind Abbr) u) (drop_gen_refl c1 (CHead d1 (Bind Abbr) u) H)) in
37 (let H_x \def (csuba_gen_abbr g d1 c2 u H1) in (let H2 \def H_x in (ex2_ind C
38 (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba
39 g d1 d2)) (ex2 C (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abbr) u)))
40 (\lambda (d2: C).(csuba g d1 d2))) (\lambda (x: C).(\lambda (H3: (eq C c2
41 (CHead x (Bind Abbr) u))).(\lambda (H4: (csuba g d1 x)).(eq_ind_r C (CHead x
42 (Bind Abbr) u) (\lambda (c: C).(ex2 C (\lambda (d2: C).(drop O O c (CHead d2
43 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (ex_intro2 C (\lambda
44 (d2: C).(drop O O (CHead x (Bind Abbr) u) (CHead d2 (Bind Abbr) u))) (\lambda
45 (d2: C).(csuba g d1 d2)) x (drop_refl (CHead x (Bind Abbr) u)) H4) c2 H3))))
46 H2))))))))))) (\lambda (n: nat).(\lambda (H: ((\forall (c1: C).(\forall (d1:
47 C).(\forall (u: T).((drop n O c1 (CHead d1 (Bind Abbr) u)) \to (\forall (g:
48 G).(\forall (c2: C).((csuba g c1 c2) \to (ex2 C (\lambda (d2: C).(drop n O c2
49 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
50 d2)))))))))))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (d1:
51 C).(\forall (u: T).((drop (S n) O c (CHead d1 (Bind Abbr) u)) \to (\forall
52 (g: G).(\forall (c2: C).((csuba g c c2) \to (ex2 C (\lambda (d2: C).(drop (S
53 n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))))))))))
54 (\lambda (n0: nat).(\lambda (d1: C).(\lambda (u: T).(\lambda (H0: (drop (S n)
55 O (CSort n0) (CHead d1 (Bind Abbr) u))).(\lambda (g: G).(\lambda (c2:
56 C).(\lambda (_: (csuba g (CSort n0) c2)).(and3_ind (eq C (CHead d1 (Bind
57 Abbr) u) (CSort n0)) (eq nat (S n) O) (eq nat O O) (ex2 C (\lambda (d2:
58 C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
59 d2))) (\lambda (H2: (eq C (CHead d1 (Bind Abbr) u) (CSort n0))).(\lambda (_:
60 (eq nat (S n) O)).(\lambda (_: (eq nat O O)).(let H5 \def (match H2 in eq
61 return (\lambda (c: C).(\lambda (_: (eq ? ? c)).((eq C c (CSort n0)) \to (ex2
62 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
63 C).(csuba g d1 d2)))))) with [refl_equal \Rightarrow (\lambda (H5: (eq C
64 (CHead d1 (Bind Abbr) u) (CSort n0))).(let H6 \def (eq_ind C (CHead d1 (Bind
65 Abbr) u) (\lambda (e: C).(match e in C return (\lambda (_: C).Prop) with
66 [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I (CSort n0)
67 H5) in (False_ind (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind
68 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) H6)))]) in (H5 (refl_equal C
69 (CSort n0))))))) (drop_gen_sort n0 (S n) O (CHead d1 (Bind Abbr) u)
70 H0))))))))) (\lambda (c: C).(\lambda (H0: ((\forall (d1: C).(\forall (u:
71 T).((drop (S n) O c (CHead d1 (Bind Abbr) u)) \to (\forall (g: G).(\forall
72 (c2: C).((csuba g c c2) \to (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead
73 d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))))))))))).(\lambda (k:
74 K).(\lambda (t: T).(\lambda (d1: C).(\lambda (u: T).(\lambda (H1: (drop (S n)
75 O (CHead c k t) (CHead d1 (Bind Abbr) u))).(\lambda (g: G).(\lambda (c2:
76 C).(\lambda (H2: (csuba g (CHead c k t) c2)).(K_ind (\lambda (k0: K).((csuba
77 g (CHead c k0 t) c2) \to ((drop (r k0 n) O c (CHead d1 (Bind Abbr) u)) \to
78 (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda
79 (d2: C).(csuba g d1 d2)))))) (\lambda (b: B).(\lambda (H3: (csuba g (CHead c
80 (Bind b) t) c2)).(\lambda (H4: (drop (r (Bind b) n) O c (CHead d1 (Bind Abbr)
81 u))).(B_ind (\lambda (b0: B).((csuba g (CHead c (Bind b0) t) c2) \to ((drop
82 (r (Bind b0) n) O c (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2:
83 C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
84 d2)))))) (\lambda (H5: (csuba g (CHead c (Bind Abbr) t) c2)).(\lambda (H6:
85 (drop (r (Bind Abbr) n) O c (CHead d1 (Bind Abbr) u))).(let H_x \def
86 (csuba_gen_abbr g c c2 t H5) in (let H7 \def H_x in (ex2_ind C (\lambda (d2:
87 C).(eq C c2 (CHead d2 (Bind Abbr) t))) (\lambda (d2: C).(csuba g c d2)) (ex2
88 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
89 C).(csuba g d1 d2))) (\lambda (x: C).(\lambda (H8: (eq C c2 (CHead x (Bind
90 Abbr) t))).(\lambda (H9: (csuba g c x)).(eq_ind_r C (CHead x (Bind Abbr) t)
91 (\lambda (c0: C).(ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind
92 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (let H10 \def (H c d1 u H6 g x
93 H9) in (ex2_ind C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abbr) u)))
94 (\lambda (d2: C).(csuba g d1 d2)) (ex2 C (\lambda (d2: C).(drop (S n) O
95 (CHead x (Bind Abbr) t) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g
96 d1 d2))) (\lambda (x0: C).(\lambda (H11: (drop n O x (CHead x0 (Bind Abbr)
97 u))).(\lambda (H12: (csuba g d1 x0)).(let H13 \def (refl_equal nat (r (Bind
98 Abbr) n)) in (let H14 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O x
99 (CHead x0 (Bind Abbr) u))) H11 (r (Bind Abbr) n) H13) in (ex_intro2 C
100 (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abbr)
101 u))) (\lambda (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Abbr) n x (CHead
102 x0 (Bind Abbr) u) H14 t) H12)))))) H10)) c2 H8)))) H7))))) (\lambda (H5:
103 (csuba g (CHead c (Bind Abst) t) c2)).(\lambda (H6: (drop (r (Bind Abst) n) O
104 c (CHead d1 (Bind Abbr) u))).(let H_x \def (csuba_gen_abst g c c2 t H5) in
105 (let H7 \def H_x in (or_ind (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind
106 Abst) t))) (\lambda (d2: C).(csuba g c d2))) (ex4_3 C T A (\lambda (d2:
107 C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2)))))
108 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g c d2)))) (\lambda
109 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g c t (asucc g a))))) (\lambda
110 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex2 C
111 (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
112 C).(csuba g d1 d2))) (\lambda (H8: (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2
113 (Bind Abst) t))) (\lambda (d2: C).(csuba g c d2)))).(ex2_ind C (\lambda (d2:
114 C).(eq C c2 (CHead d2 (Bind Abst) t))) (\lambda (d2: C).(csuba g c d2)) (ex2
115 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
116 C).(csuba g d1 d2))) (\lambda (x: C).(\lambda (H9: (eq C c2 (CHead x (Bind
117 Abst) t))).(\lambda (H10: (csuba g c x)).(eq_ind_r C (CHead x (Bind Abst) t)
118 (\lambda (c0: C).(ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind
119 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (let H11 \def (H c d1 u H6 g x
120 H10) in (ex2_ind C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abbr) u)))
121 (\lambda (d2: C).(csuba g d1 d2)) (ex2 C (\lambda (d2: C).(drop (S n) O
122 (CHead x (Bind Abst) t) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g
123 d1 d2))) (\lambda (x0: C).(\lambda (H12: (drop n O x (CHead x0 (Bind Abbr)
124 u))).(\lambda (H13: (csuba g d1 x0)).(let H14 \def (refl_equal nat (r (Bind
125 Abbr) n)) in (let H15 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O x
126 (CHead x0 (Bind Abbr) u))) H12 (r (Bind Abbr) n) H14) in (ex_intro2 C
127 (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abbr)
128 u))) (\lambda (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Abst) n x (CHead
129 x0 (Bind Abbr) u) H15 t) H13)))))) H11)) c2 H9)))) H8)) (\lambda (H8: (ex4_3
130 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2
131 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
132 c d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g c t (asucc
133 g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
134 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
135 A).(eq C c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
136 T).(\lambda (_: A).(csuba g c d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda
137 (a: A).(arity g c t (asucc g a))))) (\lambda (d2: C).(\lambda (u2:
138 T).(\lambda (a: A).(arity g d2 u2 a)))) (ex2 C (\lambda (d2: C).(drop (S n) O
139 c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) (\lambda
140 (x0: C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H9: (eq C c2 (CHead x0
141 (Bind Abbr) x1))).(\lambda (H10: (csuba g c x0)).(\lambda (_: (arity g c t
142 (asucc g x2))).(\lambda (_: (arity g x0 x1 x2)).(eq_ind_r C (CHead x0 (Bind
143 Abbr) x1) (\lambda (c0: C).(ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2
144 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (let H13 \def (H c d1 u
145 H6 g x0 H10) in (ex2_ind C (\lambda (d2: C).(drop n O x0 (CHead d2 (Bind
146 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) (ex2 C (\lambda (d2: C).(drop (S
147 n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abbr) u))) (\lambda (d2:
148 C).(csuba g d1 d2))) (\lambda (x: C).(\lambda (H14: (drop n O x0 (CHead x
149 (Bind Abbr) u))).(\lambda (H15: (csuba g d1 x)).(let H16 \def (refl_equal nat
150 (r (Bind Abbr) n)) in (let H17 \def (eq_ind nat n (\lambda (n0: nat).(drop n0
151 O x0 (CHead x (Bind Abbr) u))) H14 (r (Bind Abbr) n) H16) in (ex_intro2 C
152 (\lambda (d2: C).(drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind
153 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) x (drop_drop (Bind Abbr) n x0
154 (CHead x (Bind Abbr) u) H17 x1) H15)))))) H13)) c2 H9)))))))) H8)) H7)))))
155 (\lambda (H5: (csuba g (CHead c (Bind Void) t) c2)).(\lambda (H6: (drop (r
156 (Bind Void) n) O c (CHead d1 (Bind Abbr) u))).(let H_x \def (csuba_gen_void g
157 c c2 t H5) in (let H7 \def H_x in (ex2_ind C (\lambda (d2: C).(eq C c2 (CHead
158 d2 (Bind Void) t))) (\lambda (d2: C).(csuba g c d2)) (ex2 C (\lambda (d2:
159 C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
160 d2))) (\lambda (x: C).(\lambda (H8: (eq C c2 (CHead x (Bind Void)
161 t))).(\lambda (H9: (csuba g c x)).(eq_ind_r C (CHead x (Bind Void) t)
162 (\lambda (c0: C).(ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind
163 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))) (let H10 \def (H c d1 u H6 g x
164 H9) in (ex2_ind C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abbr) u)))
165 (\lambda (d2: C).(csuba g d1 d2)) (ex2 C (\lambda (d2: C).(drop (S n) O
166 (CHead x (Bind Void) t) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g
167 d1 d2))) (\lambda (x0: C).(\lambda (H11: (drop n O x (CHead x0 (Bind Abbr)
168 u))).(\lambda (H12: (csuba g d1 x0)).(let H13 \def (refl_equal nat (r (Bind
169 Abbr) n)) in (let H14 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O x
170 (CHead x0 (Bind Abbr) u))) H11 (r (Bind Abbr) n) H13) in (ex_intro2 C
171 (\lambda (d2: C).(drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abbr)
172 u))) (\lambda (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Void) n x (CHead
173 x0 (Bind Abbr) u) H14 t) H12)))))) H10)) c2 H8)))) H7))))) b H3 H4))))
174 (\lambda (f: F).(\lambda (H3: (csuba g (CHead c (Flat f) t) c2)).(\lambda
175 (H4: (drop (r (Flat f) n) O c (CHead d1 (Bind Abbr) u))).(let H_x \def
176 (csuba_gen_flat g c c2 t f H3) in (let H5 \def H_x in (ex2_2_ind C T (\lambda
177 (d2: C).(\lambda (u2: T).(eq C c2 (CHead d2 (Flat f) u2)))) (\lambda (d2:
178 C).(\lambda (_: T).(csuba g c d2))) (ex2 C (\lambda (d2: C).(drop (S n) O c2
179 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) (\lambda (x0:
180 C).(\lambda (x1: T).(\lambda (H6: (eq C c2 (CHead x0 (Flat f) x1))).(\lambda
181 (H7: (csuba g c x0)).(eq_ind_r C (CHead x0 (Flat f) x1) (\lambda (c0: C).(ex2
182 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
183 C).(csuba g d1 d2)))) (let H8 \def (H0 d1 u H4 g x0 H7) in (ex2_ind C
184 (\lambda (d2: C).(drop (S n) O x0 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
185 C).(csuba g d1 d2)) (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Flat f)
186 x1) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) (\lambda
187 (x: C).(\lambda (H9: (drop (S n) O x0 (CHead x (Bind Abbr) u))).(\lambda
188 (H10: (csuba g d1 x)).(ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x0
189 (Flat f) x1) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) x
190 (drop_drop (Flat f) n x0 (CHead x (Bind Abbr) u) H9 x1) H10)))) H8)) c2
191 H6))))) H5)))))) k H2 (drop_gen_drop k c (CHead d1 (Bind Abbr) u) t n
192 H1)))))))))))) c1)))) i).
194 theorem csuba_drop_abst:
195 \forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).((drop i
196 O c1 (CHead d1 (Bind Abst) u1)) \to (\forall (g: G).(\forall (c2: C).((csuba
197 g c1 c2) \to (or (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abst)
198 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
199 C).(\lambda (u2: T).(\lambda (_: A).(drop i O c2 (CHead d2 (Bind Abbr)
200 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
201 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
202 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
205 \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (d1:
206 C).(\forall (u1: T).((drop n O c1 (CHead d1 (Bind Abst) u1)) \to (\forall (g:
207 G).(\forall (c2: C).((csuba g c1 c2) \to (or (ex2 C (\lambda (d2: C).(drop n
208 O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C
209 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O c2 (CHead d2
210 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
211 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
212 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
213 u2 a)))))))))))))) (\lambda (c1: C).(\lambda (d1: C).(\lambda (u1:
214 T).(\lambda (H: (drop O O c1 (CHead d1 (Bind Abst) u1))).(\lambda (g:
215 G).(\lambda (c2: C).(\lambda (H0: (csuba g c1 c2)).(let H1 \def (eq_ind C c1
216 (\lambda (c: C).(csuba g c c2)) H0 (CHead d1 (Bind Abst) u1) (drop_gen_refl
217 c1 (CHead d1 (Bind Abst) u1) H)) in (let H_x \def (csuba_gen_abst g d1 c2 u1
218 H1) in (let H2 \def H_x in (or_ind (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2
219 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
220 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr)
221 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
222 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
223 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
224 a))))) (or (ex2 C (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abst) u1)))
225 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
226 (u2: T).(\lambda (_: A).(drop O O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda
227 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
228 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
229 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (H3:
230 (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
231 C).(csuba g d1 d2)))).(ex2_ind C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind
232 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) (or (ex2 C (\lambda (d2:
233 C).(drop O O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
234 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O
235 O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
236 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
237 A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
238 (a: A).(arity g d2 u2 a)))))) (\lambda (x: C).(\lambda (H4: (eq C c2 (CHead x
239 (Bind Abst) u1))).(\lambda (H5: (csuba g d1 x)).(eq_ind_r C (CHead x (Bind
240 Abst) u1) (\lambda (c: C).(or (ex2 C (\lambda (d2: C).(drop O O c (CHead d2
241 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
242 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O c (CHead d2 (Bind Abbr)
243 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
244 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
245 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
246 a))))))) (or_introl (ex2 C (\lambda (d2: C).(drop O O (CHead x (Bind Abst)
247 u1) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T
248 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O (CHead x (Bind
249 Abst) u1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
250 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
251 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
252 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex_intro2 C (\lambda (d2:
253 C).(drop O O (CHead x (Bind Abst) u1) (CHead d2 (Bind Abst) u1))) (\lambda
254 (d2: C).(csuba g d1 d2)) x (drop_refl (CHead x (Bind Abst) u1)) H5)) c2
255 H4)))) H3)) (\lambda (H3: (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
256 T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
257 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
258 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
259 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))).(ex4_3_ind C
260 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2
261 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
262 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
263 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
264 u2 a)))) (or (ex2 C (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abst) u1)))
265 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
266 (u2: T).(\lambda (_: A).(drop O O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda
267 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
268 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
269 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x0:
270 C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H4: (eq C c2 (CHead x0 (Bind
271 Abbr) x1))).(\lambda (H5: (csuba g d1 x0)).(\lambda (H6: (arity g d1 u1
272 (asucc g x2))).(\lambda (H7: (arity g x0 x1 x2)).(eq_ind_r C (CHead x0 (Bind
273 Abbr) x1) (\lambda (c: C).(or (ex2 C (\lambda (d2: C).(drop O O c (CHead d2
274 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
275 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O c (CHead d2 (Bind Abbr)
276 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
277 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
278 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
279 a))))))) (or_intror (ex2 C (\lambda (d2: C).(drop O O (CHead x0 (Bind Abbr)
280 x1) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T
281 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O (CHead x0 (Bind
282 Abbr) x1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
283 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
284 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
285 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex4_3_intro C T A (\lambda
286 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O (CHead x0 (Bind Abbr) x1)
287 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
288 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
289 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
290 A).(arity g d2 u2 a)))) x0 x1 x2 (drop_refl (CHead x0 (Bind Abbr) x1)) H5 H6
291 H7)) c2 H4)))))))) H3)) H2))))))))))) (\lambda (n: nat).(\lambda (H:
292 ((\forall (c1: C).(\forall (d1: C).(\forall (u1: T).((drop n O c1 (CHead d1
293 (Bind Abst) u1)) \to (\forall (g: G).(\forall (c2: C).((csuba g c1 c2) \to
294 (or (ex2 C (\lambda (d2: C).(drop n O c2 (CHead d2 (Bind Abst) u1))) (\lambda
295 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
296 T).(\lambda (_: A).(drop n O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
297 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
298 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
299 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
300 a))))))))))))))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (d1:
301 C).(\forall (u1: T).((drop (S n) O c (CHead d1 (Bind Abst) u1)) \to (\forall
302 (g: G).(\forall (c2: C).((csuba g c c2) \to (or (ex2 C (\lambda (d2: C).(drop
303 (S n) O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
304 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O
305 c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
306 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
307 A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
308 (a: A).(arity g d2 u2 a))))))))))))) (\lambda (n0: nat).(\lambda (d1:
309 C).(\lambda (u1: T).(\lambda (H0: (drop (S n) O (CSort n0) (CHead d1 (Bind
310 Abst) u1))).(\lambda (g: G).(\lambda (c2: C).(\lambda (_: (csuba g (CSort n0)
311 c2)).(and3_ind (eq C (CHead d1 (Bind Abst) u1) (CSort n0)) (eq nat (S n) O)
312 (eq nat O O) (or (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind
313 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
314 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c2 (CHead d2 (Bind Abbr)
315 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
316 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
317 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
318 a)))))) (\lambda (H2: (eq C (CHead d1 (Bind Abst) u1) (CSort n0))).(\lambda
319 (_: (eq nat (S n) O)).(\lambda (_: (eq nat O O)).(let H5 \def (match H2 in eq
320 return (\lambda (c: C).(\lambda (_: (eq ? ? c)).((eq C c (CSort n0)) \to (or
321 (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u1))) (\lambda
322 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
323 T).(\lambda (_: A).(drop (S n) O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda
324 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
325 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
326 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))))))) with
327 [refl_equal \Rightarrow (\lambda (H5: (eq C (CHead d1 (Bind Abst) u1) (CSort
328 n0))).(let H6 \def (eq_ind C (CHead d1 (Bind Abst) u1) (\lambda (e: C).(match
329 e in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False |
330 (CHead _ _ _) \Rightarrow True])) I (CSort n0) H5) in (False_ind (or (ex2 C
331 (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
332 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
333 (_: A).(drop (S n) O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
334 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
335 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
336 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) H6)))]) in
337 (H5 (refl_equal C (CSort n0))))))) (drop_gen_sort n0 (S n) O (CHead d1 (Bind
338 Abst) u1) H0))))))))) (\lambda (c: C).(\lambda (H0: ((\forall (d1:
339 C).(\forall (u1: T).((drop (S n) O c (CHead d1 (Bind Abst) u1)) \to (\forall
340 (g: G).(\forall (c2: C).((csuba g c c2) \to (or (ex2 C (\lambda (d2: C).(drop
341 (S n) O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
342 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O
343 c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
344 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
345 A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
346 (a: A).(arity g d2 u2 a)))))))))))))).(\lambda (k: K).(\lambda (t:
347 T).(\lambda (d1: C).(\lambda (u1: T).(\lambda (H1: (drop (S n) O (CHead c k
348 t) (CHead d1 (Bind Abst) u1))).(\lambda (g: G).(\lambda (c2: C).(\lambda (H2:
349 (csuba g (CHead c k t) c2)).(K_ind (\lambda (k0: K).((csuba g (CHead c k0 t)
350 c2) \to ((drop (r k0 n) O c (CHead d1 (Bind Abst) u1)) \to (or (ex2 C
351 (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
352 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
353 (_: A).(drop (S n) O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
354 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
355 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
356 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))))))) (\lambda
357 (b: B).(\lambda (H3: (csuba g (CHead c (Bind b) t) c2)).(\lambda (H4: (drop
358 (r (Bind b) n) O c (CHead d1 (Bind Abst) u1))).(B_ind (\lambda (b0:
359 B).((csuba g (CHead c (Bind b0) t) c2) \to ((drop (r (Bind b0) n) O c (CHead
360 d1 (Bind Abst) u1)) \to (or (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead
361 d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
362 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c2 (CHead d2 (Bind
363 Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1
364 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc
365 g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
366 a))))))))) (\lambda (H5: (csuba g (CHead c (Bind Abbr) t) c2)).(\lambda (H6:
367 (drop (r (Bind Abbr) n) O c (CHead d1 (Bind Abst) u1))).(let H_x \def
368 (csuba_gen_abbr g c c2 t H5) in (let H7 \def H_x in (ex2_ind C (\lambda (d2:
369 C).(eq C c2 (CHead d2 (Bind Abbr) t))) (\lambda (d2: C).(csuba g c d2)) (or
370 (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u1))) (\lambda
371 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
372 T).(\lambda (_: A).(drop (S n) O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda
373 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
374 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
375 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x:
376 C).(\lambda (H8: (eq C c2 (CHead x (Bind Abbr) t))).(\lambda (H9: (csuba g c
377 x)).(eq_ind_r C (CHead x (Bind Abbr) t) (\lambda (c0: C).(or (ex2 C (\lambda
378 (d2: C).(drop (S n) O c0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba
379 g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
380 A).(drop (S n) O c0 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda
381 (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
382 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
383 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))))) (let H10 \def (H c d1 u1 H6 g
384 x H9) in (or_ind (ex2 C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abst)
385 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
386 C).(\lambda (u2: T).(\lambda (_: A).(drop n O x (CHead d2 (Bind Abbr) u2)))))
387 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
388 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
389 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (or
390 (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind
391 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
392 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Abbr) t)
393 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
394 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
395 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
396 A).(arity g d2 u2 a)))))) (\lambda (H11: (ex2 C (\lambda (d2: C).(drop n O x
397 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))).(ex2_ind C
398 (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abst) u1))) (\lambda (d2:
399 C).(csuba g d1 d2)) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind
400 Abbr) t) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
401 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O
402 (CHead x (Bind Abbr) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
403 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
404 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
405 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x0:
406 C).(\lambda (H12: (drop n O x (CHead x0 (Bind Abst) u1))).(\lambda (H13:
407 (csuba g d1 x0)).(let H14 \def (refl_equal nat (r (Bind Abbr) n)) in (let H15
408 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O x (CHead x0 (Bind Abst)
409 u1))) H12 (r (Bind Abbr) n) H14) in (or_introl (ex2 C (\lambda (d2: C).(drop
410 (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1))) (\lambda (d2:
411 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
412 (_: A).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abbr) u2)))))
413 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
414 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
415 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))
416 (ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2
417 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Abbr)
418 n x (CHead x0 (Bind Abst) u1) H15 t) H13))))))) H11)) (\lambda (H11: (ex4_3 C
419 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O x (CHead d2
420 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
421 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
422 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
423 u2 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
424 A).(drop n O x (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
425 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
426 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
427 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) (or (ex2 C (\lambda (d2:
428 C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1))) (\lambda
429 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
430 T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind
431 Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1
432 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc
433 g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
434 a)))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H12:
435 (drop n O x (CHead x0 (Bind Abbr) x1))).(\lambda (H13: (csuba g d1
436 x0)).(\lambda (H14: (arity g d1 u1 (asucc g x2))).(\lambda (H15: (arity g x0
437 x1 x2)).(let H16 \def (refl_equal nat (r (Bind Abbr) n)) in (let H17 \def
438 (eq_ind nat n (\lambda (n0: nat).(drop n0 O x (CHead x0 (Bind Abbr) x1))) H12
439 (r (Bind Abbr) n) H16) in (or_intror (ex2 C (\lambda (d2: C).(drop (S n) O
440 (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g
441 d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop
442 (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
443 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
444 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
445 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex4_3_intro C
446 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x
447 (Bind Abbr) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
448 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
449 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
450 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) x0 x1 x2 (drop_drop (Bind Abbr)
451 n x (CHead x0 (Bind Abbr) x1) H17 t) H13 H14 H15))))))))))) H11)) H10)) c2
452 H8)))) H7))))) (\lambda (H5: (csuba g (CHead c (Bind Abst) t) c2)).(\lambda
453 (H6: (drop (r (Bind Abst) n) O c (CHead d1 (Bind Abst) u1))).(let H_x \def
454 (csuba_gen_abst g c c2 t H5) in (let H7 \def H_x in (or_ind (ex2 C (\lambda
455 (d2: C).(eq C c2 (CHead d2 (Bind Abst) t))) (\lambda (d2: C).(csuba g c d2)))
456 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2
457 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
458 A).(csuba g c d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g
459 c t (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity
460 g d2 u2 a))))) (or (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind
461 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
462 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c2 (CHead d2 (Bind Abbr)
463 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
464 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
465 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
466 a)))))) (\lambda (H8: (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst)
467 t))) (\lambda (d2: C).(csuba g c d2)))).(ex2_ind C (\lambda (d2: C).(eq C c2
468 (CHead d2 (Bind Abst) t))) (\lambda (d2: C).(csuba g c d2)) (or (ex2 C
469 (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
470 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
471 (_: A).(drop (S n) O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
472 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
473 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
474 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x:
475 C).(\lambda (H9: (eq C c2 (CHead x (Bind Abst) t))).(\lambda (H10: (csuba g c
476 x)).(eq_ind_r C (CHead x (Bind Abst) t) (\lambda (c0: C).(or (ex2 C (\lambda
477 (d2: C).(drop (S n) O c0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba
478 g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
479 A).(drop (S n) O c0 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda
480 (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
481 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
482 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))))) (let H11 \def (H c d1 u1 H6 g
483 x H10) in (or_ind (ex2 C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abst)
484 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
485 C).(\lambda (u2: T).(\lambda (_: A).(drop n O x (CHead d2 (Bind Abbr) u2)))))
486 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
487 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
488 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (or
489 (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind
490 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
491 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Abst) t)
492 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
493 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
494 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
495 A).(arity g d2 u2 a)))))) (\lambda (H12: (ex2 C (\lambda (d2: C).(drop n O x
496 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))).(ex2_ind C
497 (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abst) u1))) (\lambda (d2:
498 C).(csuba g d1 d2)) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind
499 Abst) t) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
500 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O
501 (CHead x (Bind Abst) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
502 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
503 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
504 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x0:
505 C).(\lambda (H13: (drop n O x (CHead x0 (Bind Abst) u1))).(\lambda (H14:
506 (csuba g d1 x0)).(let H15 \def (refl_equal nat (r (Bind Abbr) n)) in (let H16
507 \def (eq_ind nat n (\lambda (n0: nat).(drop n0 O x (CHead x0 (Bind Abst)
508 u1))) H13 (r (Bind Abbr) n) H15) in (or_introl (ex2 C (\lambda (d2: C).(drop
509 (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1))) (\lambda (d2:
510 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
511 (_: A).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abbr) u2)))))
512 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
513 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
514 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))
515 (ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2
516 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Abst)
517 n x (CHead x0 (Bind Abst) u1) H16 t) H14))))))) H12)) (\lambda (H12: (ex4_3 C
518 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O x (CHead d2
519 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
520 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
521 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
522 u2 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
523 A).(drop n O x (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
524 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
525 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
526 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) (or (ex2 C (\lambda (d2:
527 C).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1))) (\lambda
528 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
529 T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind
530 Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1
531 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc
532 g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
533 a)))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H13:
534 (drop n O x (CHead x0 (Bind Abbr) x1))).(\lambda (H14: (csuba g d1
535 x0)).(\lambda (H15: (arity g d1 u1 (asucc g x2))).(\lambda (H16: (arity g x0
536 x1 x2)).(let H17 \def (refl_equal nat (r (Bind Abbr) n)) in (let H18 \def
537 (eq_ind nat n (\lambda (n0: nat).(drop n0 O x (CHead x0 (Bind Abbr) x1))) H13
538 (r (Bind Abbr) n) H17) in (or_intror (ex2 C (\lambda (d2: C).(drop (S n) O
539 (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g
540 d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop
541 (S n) O (CHead x (Bind Abst) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
542 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
543 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
544 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex4_3_intro C
545 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x
546 (Bind Abst) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
547 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
548 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
549 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) x0 x1 x2 (drop_drop (Bind Abst)
550 n x (CHead x0 (Bind Abbr) x1) H18 t) H14 H15 H16))))))))))) H12)) H11)) c2
551 H9)))) H8)) (\lambda (H8: (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
552 T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
553 C).(\lambda (_: T).(\lambda (_: A).(csuba g c d2)))) (\lambda (_: C).(\lambda
554 (_: T).(\lambda (a: A).(arity g c t (asucc g a))))) (\lambda (d2: C).(\lambda
555 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))).(ex4_3_ind C T A (\lambda (d2:
556 C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2)))))
557 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g c d2)))) (\lambda
558 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g c t (asucc g a))))) (\lambda
559 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) (or (ex2 C
560 (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
561 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
562 (_: A).(drop (S n) O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
563 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
564 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
565 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x0:
566 C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H9: (eq C c2 (CHead x0 (Bind
567 Abbr) x1))).(\lambda (H10: (csuba g c x0)).(\lambda (_: (arity g c t (asucc g
568 x2))).(\lambda (_: (arity g x0 x1 x2)).(eq_ind_r C (CHead x0 (Bind Abbr) x1)
569 (\lambda (c0: C).(or (ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind
570 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
571 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c0 (CHead d2 (Bind Abbr)
572 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
573 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
574 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
575 a))))))) (let H13 \def (H c d1 u1 H6 g x0 H10) in (or_ind (ex2 C (\lambda
576 (d2: C).(drop n O x0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
577 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n
578 O x0 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
579 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
580 A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
581 (a: A).(arity g d2 u2 a))))) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead
582 x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
583 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S
584 n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
585 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
586 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
587 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda
588 (H14: (ex2 C (\lambda (d2: C).(drop n O x0 (CHead d2 (Bind Abst) u1)))
589 (\lambda (d2: C).(csuba g d1 d2)))).(ex2_ind C (\lambda (d2: C).(drop n O x0
590 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) (or (ex2 C
591 (\lambda (d2: C).(drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind
592 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
593 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0 (Bind Abbr) x1)
594 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
595 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
596 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
597 A).(arity g d2 u2 a)))))) (\lambda (x: C).(\lambda (H15: (drop n O x0 (CHead
598 x (Bind Abst) u1))).(\lambda (H16: (csuba g d1 x)).(let H17 \def (refl_equal
599 nat (r (Bind Abbr) n)) in (let H18 \def (eq_ind nat n (\lambda (n0:
600 nat).(drop n0 O x0 (CHead x (Bind Abst) u1))) H15 (r (Bind Abbr) n) H17) in
601 (or_introl (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Bind Abbr) x1)
602 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
603 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0
604 (Bind Abbr) x1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
605 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
606 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
607 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex_intro2 C (\lambda (d2:
608 C).(drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)))
609 (\lambda (d2: C).(csuba g d1 d2)) x (drop_drop (Bind Abbr) n x0 (CHead x
610 (Bind Abst) u1) H18 x1) H16))))))) H14)) (\lambda (H14: (ex4_3 C T A (\lambda
611 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O x0 (CHead d2 (Bind Abbr)
612 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
613 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
614 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
615 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
616 A).(drop n O x0 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
617 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
618 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
619 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) (or (ex2 C (\lambda (d2:
620 C).(drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1)))
621 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
622 (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2
623 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
624 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
625 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
626 u2 a)))))) (\lambda (x3: C).(\lambda (x4: T).(\lambda (x5: A).(\lambda (H15:
627 (drop n O x0 (CHead x3 (Bind Abbr) x4))).(\lambda (H16: (csuba g d1
628 x3)).(\lambda (H17: (arity g d1 u1 (asucc g x5))).(\lambda (H18: (arity g x3
629 x4 x5)).(let H19 \def (refl_equal nat (r (Bind Abbr) n)) in (let H20 \def
630 (eq_ind nat n (\lambda (n0: nat).(drop n0 O x0 (CHead x3 (Bind Abbr) x4)))
631 H15 (r (Bind Abbr) n) H19) in (or_intror (ex2 C (\lambda (d2: C).(drop (S n)
632 O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) u1))) (\lambda (d2:
633 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
634 (_: A).(drop (S n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abbr) u2)))))
635 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
636 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
637 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))
638 (ex4_3_intro C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S
639 n) O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
640 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
641 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
642 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) x3 x4 x5
643 (drop_drop (Bind Abbr) n x0 (CHead x3 (Bind Abbr) x4) H20 x1) H16 H17
644 H18))))))))))) H14)) H13)) c2 H9)))))))) H8)) H7))))) (\lambda (H5: (csuba g
645 (CHead c (Bind Void) t) c2)).(\lambda (H6: (drop (r (Bind Void) n) O c (CHead
646 d1 (Bind Abst) u1))).(let H_x \def (csuba_gen_void g c c2 t H5) in (let H7
647 \def H_x in (ex2_ind C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Void) t)))
648 (\lambda (d2: C).(csuba g c d2)) (or (ex2 C (\lambda (d2: C).(drop (S n) O c2
649 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
650 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c2 (CHead d2
651 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
652 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
653 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
654 u2 a)))))) (\lambda (x: C).(\lambda (H8: (eq C c2 (CHead x (Bind Void)
655 t))).(\lambda (H9: (csuba g c x)).(eq_ind_r C (CHead x (Bind Void) t)
656 (\lambda (c0: C).(or (ex2 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind
657 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
658 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c0 (CHead d2 (Bind Abbr)
659 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
660 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
661 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
662 a))))))) (let H10 \def (H c d1 u1 H6 g x H9) in (or_ind (ex2 C (\lambda (d2:
663 C).(drop n O x (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
664 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O x
665 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
666 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
667 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
668 A).(arity g d2 u2 a))))) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x
669 (Bind Void) t) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
670 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O
671 (CHead x (Bind Void) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
672 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
673 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
674 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda
675 (H11: (ex2 C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abst) u1)))
676 (\lambda (d2: C).(csuba g d1 d2)))).(ex2_ind C (\lambda (d2: C).(drop n O x
677 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) (or (ex2 C
678 (\lambda (d2: C).(drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst)
679 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
680 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Void) t)
681 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
682 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
683 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
684 A).(arity g d2 u2 a)))))) (\lambda (x0: C).(\lambda (H12: (drop n O x (CHead
685 x0 (Bind Abst) u1))).(\lambda (H13: (csuba g d1 x0)).(let H14 \def
686 (refl_equal nat (r (Bind Abbr) n)) in (let H15 \def (eq_ind nat n (\lambda
687 (n0: nat).(drop n0 O x (CHead x0 (Bind Abst) u1))) H12 (r (Bind Abbr) n) H14)
688 in (or_introl (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Void) t)
689 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
690 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x
691 (Bind Void) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
692 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
693 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
694 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex_intro2 C (\lambda (d2:
695 C).(drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u1))) (\lambda
696 (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Void) n x (CHead x0 (Bind Abst)
697 u1) H15 t) H13))))))) H11)) (\lambda (H11: (ex4_3 C T A (\lambda (d2:
698 C).(\lambda (u2: T).(\lambda (_: A).(drop n O x (CHead d2 (Bind Abbr) u2)))))
699 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
700 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
701 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
702 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
703 A).(drop n O x (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
704 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
705 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
706 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) (or (ex2 C (\lambda (d2:
707 C).(drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u1))) (\lambda
708 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
709 T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind
710 Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1
711 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc
712 g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
713 a)))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: A).(\lambda (H12:
714 (drop n O x (CHead x0 (Bind Abbr) x1))).(\lambda (H13: (csuba g d1
715 x0)).(\lambda (H14: (arity g d1 u1 (asucc g x2))).(\lambda (H15: (arity g x0
716 x1 x2)).(let H16 \def (refl_equal nat (r (Bind Abbr) n)) in (let H17 \def
717 (eq_ind nat n (\lambda (n0: nat).(drop n0 O x (CHead x0 (Bind Abbr) x1))) H12
718 (r (Bind Abbr) n) H16) in (or_intror (ex2 C (\lambda (d2: C).(drop (S n) O
719 (CHead x (Bind Void) t) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g
720 d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop
721 (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
722 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
723 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
724 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex4_3_intro C
725 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x
726 (Bind Void) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
727 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
728 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
729 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) x0 x1 x2 (drop_drop (Bind Void)
730 n x (CHead x0 (Bind Abbr) x1) H17 t) H13 H14 H15))))))))))) H11)) H10)) c2
731 H8)))) H7))))) b H3 H4)))) (\lambda (f: F).(\lambda (H3: (csuba g (CHead c
732 (Flat f) t) c2)).(\lambda (H4: (drop (r (Flat f) n) O c (CHead d1 (Bind Abst)
733 u1))).(let H_x \def (csuba_gen_flat g c c2 t f H3) in (let H5 \def H_x in
734 (ex2_2_ind C T (\lambda (d2: C).(\lambda (u2: T).(eq C c2 (CHead d2 (Flat f)
735 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g c d2))) (or (ex2 C (\lambda
736 (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba
737 g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
738 A).(drop (S n) O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda
739 (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
740 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
741 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x0: C).(\lambda (x1:
742 T).(\lambda (H6: (eq C c2 (CHead x0 (Flat f) x1))).(\lambda (H7: (csuba g c
743 x0)).(eq_ind_r C (CHead x0 (Flat f) x1) (\lambda (c0: C).(or (ex2 C (\lambda
744 (d2: C).(drop (S n) O c0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba
745 g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
746 A).(drop (S n) O c0 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda
747 (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
748 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
749 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))))) (let H8 \def (H0 d1 u1 H4 g
750 x0 H7) in (or_ind (ex2 C (\lambda (d2: C).(drop (S n) O x0 (CHead d2 (Bind
751 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
752 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O x0 (CHead d2 (Bind Abbr)
753 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
754 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
755 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
756 a))))) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Flat f) x1)
757 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
758 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0
759 (Flat f) x1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
760 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
761 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
762 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (H9: (ex2 C (\lambda
763 (d2: C).(drop (S n) O x0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba
764 g d1 d2)))).(ex2_ind C (\lambda (d2: C).(drop (S n) O x0 (CHead d2 (Bind
765 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) (or (ex2 C (\lambda (d2:
766 C).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1))) (\lambda
767 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
768 T).(\lambda (_: A).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abbr)
769 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
770 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
771 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
772 a)))))) (\lambda (x: C).(\lambda (H10: (drop (S n) O x0 (CHead x (Bind Abst)
773 u1))).(\lambda (H11: (csuba g d1 x)).(or_introl (ex2 C (\lambda (d2: C).(drop
774 (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1))) (\lambda (d2:
775 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
776 (_: A).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abbr) u2)))))
777 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
778 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
779 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))
780 (ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2
781 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) x (drop_drop (Flat f) n
782 x0 (CHead x (Bind Abst) u1) H10 x1) H11))))) H9)) (\lambda (H9: (ex4_3 C T A
783 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O x0 (CHead d2
784 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
785 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
786 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
787 u2 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
788 A).(drop (S n) O x0 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda
789 (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
790 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
791 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) (or (ex2 C (\lambda (d2:
792 C).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1))) (\lambda
793 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
794 T).(\lambda (_: A).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abbr)
795 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
796 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
797 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
798 a)))))) (\lambda (x2: C).(\lambda (x3: T).(\lambda (x4: A).(\lambda (H10:
799 (drop (S n) O x0 (CHead x2 (Bind Abbr) x3))).(\lambda (H11: (csuba g d1
800 x2)).(\lambda (H12: (arity g d1 u1 (asucc g x4))).(\lambda (H13: (arity g x2
801 x3 x4)).(or_intror (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Flat f)
802 x1) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T
803 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0
804 (Flat f) x1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
805 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
806 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
807 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex4_3_intro C T A (\lambda
808 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0 (Flat f) x1)
809 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
810 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
811 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
812 A).(arity g d2 u2 a)))) x2 x3 x4 (drop_drop (Flat f) n x0 (CHead x2 (Bind
813 Abbr) x3) H10 x1) H11 H12 H13))))))))) H9)) H8)) c2 H6))))) H5)))))) k H2
814 (drop_gen_drop k c (CHead d1 (Bind Abst) u1) t n H1)))))))))))) c1)))) i).
projects / helm.git / blob