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 H2 \def (csuba_gen_abbr g d1 c2 u H1) in (ex2_ind C (\lambda (d2: C).(eq
38 C c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) (ex2 C
39 (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
40 C).(csuba g d1 d2))) (\lambda (x: C).(\lambda (H3: (eq C c2 (CHead x (Bind
41 Abbr) u))).(\lambda (H4: (csuba g d1 x)).(eq_ind_r C (CHead x (Bind Abbr) u)
42 (\lambda (c: C).(ex2 C (\lambda (d2: C).(drop O O c (CHead d2 (Bind Abbr)
43 u))) (\lambda (d2: C).(csuba g d1 d2)))) (ex_intro2 C (\lambda (d2: C).(drop
44 O O (CHead x (Bind Abbr) u) (CHead d2 (Bind Abbr) u))) (\lambda (d2:
45 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 H7 \def
86 (csuba_gen_abbr g c c2 t H5) in (ex2_ind C (\lambda (d2: C).(eq C c2 (CHead
87 d2 (Bind Abbr) t))) (\lambda (d2: C).(csuba g c d2)) (ex2 C (\lambda (d2:
88 C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
89 d2))) (\lambda (x: C).(\lambda (H8: (eq C c2 (CHead x (Bind Abbr)
90 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 H7 \def (csuba_gen_abst g c c2 t H5) in
105 (or_ind (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) t))) (\lambda
106 (d2: C).(csuba g c d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
107 T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
108 C).(\lambda (_: T).(\lambda (_: A).(csuba g c d2)))) (\lambda (_: C).(\lambda
109 (_: T).(\lambda (a: A).(arity g c t (asucc g a))))) (\lambda (d2: C).(\lambda
110 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex2 C (\lambda (d2: C).(drop
111 (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))
112 (\lambda (H8: (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) t)))
113 (\lambda (d2: C).(csuba g c d2)))).(ex2_ind C (\lambda (d2: C).(eq C c2
114 (CHead d2 (Bind Abst) t))) (\lambda (d2: C).(csuba g c d2)) (ex2 C (\lambda
115 (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g
116 d1 d2))) (\lambda (x: C).(\lambda (H9: (eq C c2 (CHead x (Bind Abst)
117 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 H7 \def (csuba_gen_void g
157 c c2 t H5) in (ex2_ind C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Void) t)))
158 (\lambda (d2: C).(csuba g c d2)) (ex2 C (\lambda (d2: C).(drop (S n) O c2
159 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) (\lambda (x:
160 C).(\lambda (H8: (eq C c2 (CHead x (Bind Void) t))).(\lambda (H9: (csuba g c
161 x)).(eq_ind_r C (CHead x (Bind Void) t) (\lambda (c0: C).(ex2 C (\lambda (d2:
162 C).(drop (S n) O c0 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
163 d2)))) (let H10 \def (H c d1 u H6 g x H9) in (ex2_ind C (\lambda (d2:
164 C).(drop n O x (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))
165 (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Void) t) (CHead d2 (Bind
166 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) (\lambda (x0: C).(\lambda (H11:
167 (drop n O x (CHead x0 (Bind Abbr) u))).(\lambda (H12: (csuba g d1 x0)).(let
168 H13 \def (refl_equal nat (r (Bind Abbr) n)) in (let H14 \def (eq_ind nat n
169 (\lambda (n0: nat).(drop n0 O x (CHead x0 (Bind Abbr) u))) H11 (r (Bind Abbr)
170 n) H13) in (ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Void)
171 t) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) x0 (drop_drop
172 (Bind Void) n x (CHead x0 (Bind Abbr) u) H14 t) H12)))))) H10)) c2 H8))))
173 H7)))) b H3 H4)))) (\lambda (f: F).(\lambda (H3: (csuba g (CHead c (Flat f)
174 t) c2)).(\lambda (H4: (drop (r (Flat f) n) O c (CHead d1 (Bind Abbr)
175 u))).(let H5 \def (csuba_gen_flat g c c2 t f H3) in (ex2_2_ind C T (\lambda
176 (d2: C).(\lambda (u2: T).(eq C c2 (CHead d2 (Flat f) u2)))) (\lambda (d2:
177 C).(\lambda (_: T).(csuba g c d2))) (ex2 C (\lambda (d2: C).(drop (S n) O c2
178 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) (\lambda (x0:
179 C).(\lambda (x1: T).(\lambda (H6: (eq C c2 (CHead x0 (Flat f) x1))).(\lambda
180 (H7: (csuba g c x0)).(eq_ind_r C (CHead x0 (Flat f) x1) (\lambda (c0: C).(ex2
181 C (\lambda (d2: C).(drop (S n) O c0 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
182 C).(csuba g d1 d2)))) (let H8 \def (H0 d1 u H4 g x0 H7) in (ex2_ind C
183 (\lambda (d2: C).(drop (S n) O x0 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
184 C).(csuba g d1 d2)) (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Flat f)
185 x1) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) (\lambda
186 (x: C).(\lambda (H9: (drop (S n) O x0 (CHead x (Bind Abbr) u))).(\lambda
187 (H10: (csuba g d1 x)).(ex_intro2 C (\lambda (d2: C).(drop (S n) O (CHead x0
188 (Flat f) x1) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) x
189 (drop_drop (Flat f) n x0 (CHead x (Bind Abbr) u) H9 x1) H10)))) H8)) c2
190 H6))))) H5))))) k H2 (drop_gen_drop k c (CHead d1 (Bind Abbr) u) t n
191 H1)))))))))))) c1)))) i).
193 theorem csuba_drop_abst:
194 \forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).((drop i
195 O c1 (CHead d1 (Bind Abst) u1)) \to (\forall (g: G).(\forall (c2: C).((csuba
196 g c1 c2) \to (or (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abst)
197 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
198 C).(\lambda (u2: T).(\lambda (_: A).(drop i O c2 (CHead d2 (Bind Abbr)
199 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
200 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
201 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
204 \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (d1:
205 C).(\forall (u1: T).((drop n O c1 (CHead d1 (Bind Abst) u1)) \to (\forall (g:
206 G).(\forall (c2: C).((csuba g c1 c2) \to (or (ex2 C (\lambda (d2: C).(drop n
207 O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C
208 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O c2 (CHead d2
209 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
210 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
211 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
212 u2 a)))))))))))))) (\lambda (c1: C).(\lambda (d1: C).(\lambda (u1:
213 T).(\lambda (H: (drop O O c1 (CHead d1 (Bind Abst) u1))).(\lambda (g:
214 G).(\lambda (c2: C).(\lambda (H0: (csuba g c1 c2)).(let H1 \def (eq_ind C c1
215 (\lambda (c: C).(csuba g c c2)) H0 (CHead d1 (Bind Abst) u1) (drop_gen_refl
216 c1 (CHead d1 (Bind Abst) u1) H)) in (let H2 \def (csuba_gen_abst g d1 c2 u1
217 H1) in (or_ind (ex2 C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) u1)))
218 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
219 (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
220 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
221 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
222 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (or (ex2 C
223 (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
224 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
225 (_: A).(drop O O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda
226 (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
227 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
228 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (H3: (ex2 C (\lambda
229 (d2: C).(eq C c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
230 d2)))).(ex2_ind C (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Abst) u1)))
231 (\lambda (d2: C).(csuba g d1 d2)) (or (ex2 C (\lambda (d2: C).(drop O O c2
232 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
233 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O c2 (CHead d2
234 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
235 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
236 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
237 u2 a)))))) (\lambda (x: C).(\lambda (H4: (eq C c2 (CHead x (Bind Abst)
238 u1))).(\lambda (H5: (csuba g d1 x)).(eq_ind_r C (CHead x (Bind Abst) u1)
239 (\lambda (c: C).(or (ex2 C (\lambda (d2: C).(drop O O c (CHead d2 (Bind Abst)
240 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
241 C).(\lambda (u2: T).(\lambda (_: A).(drop O O c (CHead d2 (Bind Abbr) u2)))))
242 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
243 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
244 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))))
245 (or_introl (ex2 C (\lambda (d2: C).(drop O O (CHead x (Bind Abst) u1) (CHead
246 d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
247 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O (CHead x (Bind Abst) u1)
248 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
249 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
250 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
251 A).(arity g d2 u2 a))))) (ex_intro2 C (\lambda (d2: C).(drop O O (CHead x
252 (Bind Abst) u1) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))
253 x (drop_refl (CHead x (Bind Abst) u1)) H5)) c2 H4)))) H3)) (\lambda (H3:
254 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2
255 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
256 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
257 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
258 A).(arity g d2 u2 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2:
259 T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
260 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
261 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
262 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) (or (ex2 C
263 (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
264 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
265 (_: A).(drop O O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda
266 (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
267 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
268 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x0: C).(\lambda (x1:
269 T).(\lambda (x2: A).(\lambda (H4: (eq C c2 (CHead x0 (Bind Abbr)
270 x1))).(\lambda (H5: (csuba g d1 x0)).(\lambda (H6: (arity g d1 u1 (asucc g
271 x2))).(\lambda (H7: (arity g x0 x1 x2)).(eq_ind_r C (CHead x0 (Bind Abbr) x1)
272 (\lambda (c: C).(or (ex2 C (\lambda (d2: C).(drop O O c (CHead d2 (Bind Abst)
273 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
274 C).(\lambda (u2: T).(\lambda (_: A).(drop O O c (CHead d2 (Bind Abbr) u2)))))
275 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
276 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
277 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))))
278 (or_intror (ex2 C (\lambda (d2: C).(drop O O (CHead x0 (Bind Abbr) x1) (CHead
279 d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
280 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop O O (CHead x0 (Bind Abbr) x1)
281 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
282 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
283 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
284 A).(arity g d2 u2 a))))) (ex4_3_intro C T A (\lambda (d2: C).(\lambda (u2:
285 T).(\lambda (_: A).(drop O O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abbr)
286 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
287 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
288 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))
289 x0 x1 x2 (drop_refl (CHead x0 (Bind Abbr) x1)) H5 H6 H7)) c2 H4)))))))) H3))
290 H2)))))))))) (\lambda (n: nat).(\lambda (H: ((\forall (c1: C).(\forall (d1:
291 C).(\forall (u1: T).((drop n O c1 (CHead d1 (Bind Abst) u1)) \to (\forall (g:
292 G).(\forall (c2: C).((csuba g c1 c2) \to (or (ex2 C (\lambda (d2: C).(drop n
293 O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C
294 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop n O c2 (CHead d2
295 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
296 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
297 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
298 u2 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 H7 \def
366 (csuba_gen_abbr g c c2 t H5) in (ex2_ind C (\lambda (d2: C).(eq C c2 (CHead
367 d2 (Bind Abbr) t))) (\lambda (d2: C).(csuba g c d2)) (or (ex2 C (\lambda (d2:
368 C).(drop (S n) O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
369 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S
370 n) O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
371 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
372 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
373 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x: C).(\lambda (H8:
374 (eq C c2 (CHead x (Bind Abbr) t))).(\lambda (H9: (csuba g c x)).(eq_ind_r C
375 (CHead x (Bind Abbr) t) (\lambda (c0: C).(or (ex2 C (\lambda (d2: C).(drop (S
376 n) O c0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3
377 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c0
378 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
379 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
380 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
381 A).(arity g d2 u2 a))))))) (let H10 \def (H c d1 u1 H6 g x H9) in (or_ind
382 (ex2 C (\lambda (d2: C).(drop n O x (CHead d2 (Bind Abst) u1))) (\lambda (d2:
383 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
384 (_: A).(drop n O x (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda
385 (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
386 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
387 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (or (ex2 C (\lambda (d2:
388 C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1))) (\lambda
389 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
390 T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind
391 Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1
392 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc
393 g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
394 a)))))) (\lambda (H11: (ex2 C (\lambda (d2: C).(drop n O x (CHead d2 (Bind
395 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))).(ex2_ind C (\lambda (d2:
396 C).(drop n O x (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))
397 (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2
398 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
399 (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x (Bind Abbr)
400 t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
401 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
402 A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
403 (a: A).(arity g d2 u2 a)))))) (\lambda (x0: C).(\lambda (H12: (drop n O x
404 (CHead x0 (Bind Abst) u1))).(\lambda (H13: (csuba g d1 x0)).(let H14 \def
405 (refl_equal nat (r (Bind Abbr) n)) in (let H15 \def (eq_ind nat n (\lambda
406 (n0: nat).(drop n0 O x (CHead x0 (Bind Abst) u1))) H12 (r (Bind Abbr) n) H14)
407 in (or_introl (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x (Bind Abbr) t)
408 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
409 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x
410 (Bind Abbr) t) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
411 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
412 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
413 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex_intro2 C (\lambda (d2:
414 C).(drop (S n) O (CHead x (Bind Abbr) t) (CHead d2 (Bind Abst) u1))) (\lambda
415 (d2: C).(csuba g d1 d2)) x0 (drop_drop (Bind Abbr) n x (CHead x0 (Bind Abst)
416 u1) H15 t) H13))))))) H11)) (\lambda (H11: (ex4_3 C T A (\lambda (d2:
417 C).(\lambda (u2: T).(\lambda (_: A).(drop n O x (CHead d2 (Bind Abbr) u2)))))
418 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
419 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
420 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
421 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 H7 \def
452 (csuba_gen_abst g c c2 t H5) in (or_ind (ex2 C (\lambda (d2: C).(eq C c2
453 (CHead d2 (Bind Abst) t))) (\lambda (d2: C).(csuba g c d2))) (ex4_3 C T A
454 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C c2 (CHead d2 (Bind
455 Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g c
456 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g c t (asucc g
457 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
458 a))))) (or (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst)
459 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 H7 \def (csuba_gen_void g c c2 t H5) in (ex2_ind C
645 (\lambda (d2: C).(eq C c2 (CHead d2 (Bind Void) t))) (\lambda (d2: C).(csuba
646 g c d2)) (or (ex2 C (\lambda (d2: C).(drop (S n) O c2 (CHead d2 (Bind Abst)
647 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
648 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c2 (CHead d2 (Bind Abbr)
649 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
650 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
651 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
652 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 H5 \def (csuba_gen_flat g c c2 t f H3) in (ex2_2_ind C T (\lambda
732 (d2: C).(\lambda (u2: T).(eq C c2 (CHead d2 (Flat f) u2)))) (\lambda (d2:
733 C).(\lambda (_: T).(csuba g c d2))) (or (ex2 C (\lambda (d2: C).(drop (S n) O
734 c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T
735 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c2 (CHead
736 d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
737 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
738 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
739 A).(arity g d2 u2 a)))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (eq
740 C c2 (CHead x0 (Flat f) x1))).(\lambda (H7: (csuba g c x0)).(eq_ind_r C
741 (CHead x0 (Flat f) x1) (\lambda (c0: C).(or (ex2 C (\lambda (d2: C).(drop (S
742 n) O c0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3
743 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O c0
744 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
745 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
746 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
747 A).(arity g d2 u2 a))))))) (let H8 \def (H0 d1 u1 H4 g x0 H7) in (or_ind (ex2
748 C (\lambda (d2: C).(drop (S n) O x0 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
749 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
750 (_: A).(drop (S n) O x0 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
751 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
752 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
753 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (or (ex2 C
754 (\lambda (d2: C).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst)
755 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
756 C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0 (Flat f) x1)
757 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
758 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
759 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
760 A).(arity g d2 u2 a)))))) (\lambda (H9: (ex2 C (\lambda (d2: C).(drop (S n) O
761 x0 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))).(ex2_ind C
762 (\lambda (d2: C).(drop (S n) O x0 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
763 C).(csuba g d1 d2)) (or (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Flat
764 f) x1) (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3
765 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead
766 x0 (Flat f) x1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
767 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
768 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
769 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x: C).(\lambda (H10:
770 (drop (S n) O x0 (CHead x (Bind Abst) u1))).(\lambda (H11: (csuba g d1
771 x)).(or_introl (ex2 C (\lambda (d2: C).(drop (S n) O (CHead x0 (Flat f) x1)
772 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
773 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop (S n) O (CHead x0
774 (Flat f) x1) (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
775 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
776 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
777 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex_intro2 C (\lambda (d2:
778 C).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abst) u1))) (\lambda
779 (d2: C).(csuba g d1 d2)) x (drop_drop (Flat f) n x0 (CHead x (Bind Abst) u1)
780 H10 x1) H11))))) H9)) (\lambda (H9: (ex4_3 C T A (\lambda (d2: C).(\lambda
781 (u2: T).(\lambda (_: A).(drop (S n) O x0 (CHead d2 (Bind Abbr) u2)))))
782 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
783 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
784 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
785 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).
projects / helm.git / blob