1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "basic_1A/csuba/drop.ma".
19 include "basic_1A/csuba/clear.ma".
21 include "basic_1A/getl/clear.ma".
23 lemma csuba_getl_abbr:
24 \forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall
25 (i: nat).((getl i c1 (CHead d1 (Bind Abbr) u)) \to (\forall (c2: C).((csuba g
26 c1 c2) \to (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abbr) u)))
27 (\lambda (d2: C).(csuba g d1 d2))))))))))
29 \lambda (g: G).(\lambda (c1: C).(\lambda (d1: C).(\lambda (u: T).(\lambda
30 (i: nat).(\lambda (H: (getl i c1 (CHead d1 (Bind Abbr) u))).(let H0 \def
31 (getl_gen_all c1 (CHead d1 (Bind Abbr) u) i H) in (ex2_ind C (\lambda (e:
32 C).(drop i O c1 e)) (\lambda (e: C).(clear e (CHead d1 (Bind Abbr) u)))
33 (\forall (c2: C).((csuba g c1 c2) \to (ex2 C (\lambda (d2: C).(getl i c2
34 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))))) (\lambda (x:
35 C).(\lambda (H1: (drop i O c1 x)).(\lambda (H2: (clear x (CHead d1 (Bind
36 Abbr) u))).(C_ind (\lambda (c: C).((drop i O c1 c) \to ((clear c (CHead d1
37 (Bind Abbr) u)) \to (\forall (c2: C).((csuba g c1 c2) \to (ex2 C (\lambda
38 (d2: C).(getl i c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
39 d2)))))))) (\lambda (n: nat).(\lambda (_: (drop i O c1 (CSort n))).(\lambda
40 (H4: (clear (CSort n) (CHead d1 (Bind Abbr) u))).(clear_gen_sort (CHead d1
41 (Bind Abbr) u) n H4 (\forall (c2: C).((csuba g c1 c2) \to (ex2 C (\lambda
42 (d2: C).(getl i c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1
43 d2))))))))) (\lambda (x0: C).(\lambda (_: (((drop i O c1 x0) \to ((clear x0
44 (CHead d1 (Bind Abbr) u)) \to (\forall (c2: C).((csuba g c1 c2) \to (ex2 C
45 (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
46 C).(csuba g d1 d2))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (H3:
47 (drop i O c1 (CHead x0 k t))).(\lambda (H4: (clear (CHead x0 k t) (CHead d1
48 (Bind Abbr) u))).(K_ind (\lambda (k0: K).((drop i O c1 (CHead x0 k0 t)) \to
49 ((clear (CHead x0 k0 t) (CHead d1 (Bind Abbr) u)) \to (\forall (c2:
50 C).((csuba g c1 c2) \to (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind
51 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))))))) (\lambda (b: B).(\lambda
52 (H5: (drop i O c1 (CHead x0 (Bind b) t))).(\lambda (H6: (clear (CHead x0
53 (Bind b) t) (CHead d1 (Bind Abbr) u))).(let H7 \def (f_equal C C (\lambda (e:
54 C).(match e with [(CSort _) \Rightarrow d1 | (CHead c _ _) \Rightarrow c]))
55 (CHead d1 (Bind Abbr) u) (CHead x0 (Bind b) t) (clear_gen_bind b x0 (CHead d1
56 (Bind Abbr) u) t H6)) in ((let H8 \def (f_equal C B (\lambda (e: C).(match e
57 with [(CSort _) \Rightarrow Abbr | (CHead _ k0 _) \Rightarrow (match k0 with
58 [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow Abbr])])) (CHead d1 (Bind
59 Abbr) u) (CHead x0 (Bind b) t) (clear_gen_bind b x0 (CHead d1 (Bind Abbr) u)
60 t H6)) in ((let H9 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _)
61 \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead d1 (Bind Abbr) u)
62 (CHead x0 (Bind b) t) (clear_gen_bind b x0 (CHead d1 (Bind Abbr) u) t H6)) in
63 (\lambda (H10: (eq B Abbr b)).(\lambda (H11: (eq C d1 x0)).(\lambda (c2:
64 C).(\lambda (H12: (csuba g c1 c2)).(let H13 \def (eq_ind_r T t (\lambda (t0:
65 T).(drop i O c1 (CHead x0 (Bind b) t0))) H5 u H9) in (let H14 \def (eq_ind_r
66 B b (\lambda (b0: B).(drop i O c1 (CHead x0 (Bind b0) u))) H13 Abbr H10) in
67 (let H15 \def (eq_ind_r C x0 (\lambda (c: C).(drop i O c1 (CHead c (Bind
68 Abbr) u))) H14 d1 H11) in (let H16 \def (csuba_drop_abbr i c1 d1 u H15 g c2
69 H12) in (ex2_ind C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abbr) u)))
70 (\lambda (d2: C).(csuba g d1 d2)) (ex2 C (\lambda (d2: C).(getl i c2 (CHead
71 d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) (\lambda (x1:
72 C).(\lambda (H17: (drop i O c2 (CHead x1 (Bind Abbr) u))).(\lambda (H18:
73 (csuba g d1 x1)).(ex_intro2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind
74 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) x1 (getl_intro i c2 (CHead x1
75 (Bind Abbr) u) (CHead x1 (Bind Abbr) u) H17 (clear_bind Abbr x1 u)) H18))))
76 H16)))))))))) H8)) H7))))) (\lambda (f: F).(\lambda (H5: (drop i O c1 (CHead
77 x0 (Flat f) t))).(\lambda (H6: (clear (CHead x0 (Flat f) t) (CHead d1 (Bind
78 Abbr) u))).(let H7 \def H5 in (unintro C c1 (\lambda (c: C).((drop i O c
79 (CHead x0 (Flat f) t)) \to (\forall (c2: C).((csuba g c c2) \to (ex2 C
80 (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
81 C).(csuba g d1 d2))))))) (nat_ind (\lambda (n: nat).(\forall (x1: C).((drop n
82 O x1 (CHead x0 (Flat f) t)) \to (\forall (c2: C).((csuba g x1 c2) \to (ex2 C
83 (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
84 C).(csuba g d1 d2)))))))) (\lambda (x1: C).(\lambda (H8: (drop O O x1 (CHead
85 x0 (Flat f) t))).(\lambda (c2: C).(\lambda (H9: (csuba g x1 c2)).(let H10
86 \def (eq_ind C x1 (\lambda (c: C).(csuba g c c2)) H9 (CHead x0 (Flat f) t)
87 (drop_gen_refl x1 (CHead x0 (Flat f) t) H8)) in (let H_y \def (clear_flat x0
88 (CHead d1 (Bind Abbr) u) (clear_gen_flat f x0 (CHead d1 (Bind Abbr) u) t H6)
89 f t) in (let H11 \def (csuba_clear_conf g (CHead x0 (Flat f) t) c2 H10 (CHead
90 d1 (Bind Abbr) u) H_y) in (ex2_ind C (\lambda (e2: C).(csuba g (CHead d1
91 (Bind Abbr) u) e2)) (\lambda (e2: C).(clear c2 e2)) (ex2 C (\lambda (d2:
92 C).(getl O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))
93 (\lambda (x2: C).(\lambda (H12: (csuba g (CHead d1 (Bind Abbr) u)
94 x2)).(\lambda (H13: (clear c2 x2)).(let H_x \def (csuba_gen_abbr g d1 x2 u
95 H12) in (let H14 \def H_x in (ex2_ind C (\lambda (d2: C).(eq C x2 (CHead d2
96 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) (ex2 C (\lambda (d2:
97 C).(getl O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)))
98 (\lambda (x3: C).(\lambda (H15: (eq C x2 (CHead x3 (Bind Abbr) u))).(\lambda
99 (H16: (csuba g d1 x3)).(let H17 \def (eq_ind C x2 (\lambda (c: C).(clear c2
100 c)) H13 (CHead x3 (Bind Abbr) u) H15) in (ex_intro2 C (\lambda (d2: C).(getl
101 O c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2)) x3
102 (getl_intro O c2 (CHead x3 (Bind Abbr) u) c2 (drop_refl c2) H17) H16)))))
103 H14)))))) H11)))))))) (\lambda (n: nat).(\lambda (H8: ((\forall (x1:
104 C).((drop n O x1 (CHead x0 (Flat f) t)) \to (\forall (c2: C).((csuba g x1 c2)
105 \to (ex2 C (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abbr) u))) (\lambda
106 (d2: C).(csuba g d1 d2))))))))).(\lambda (x1: C).(\lambda (H9: (drop (S n) O
107 x1 (CHead x0 (Flat f) t))).(\lambda (c2: C).(\lambda (H10: (csuba g x1
108 c2)).(let H11 \def (drop_clear x1 (CHead x0 (Flat f) t) n H9) in (ex2_3_ind B
109 C T (\lambda (b: B).(\lambda (e: C).(\lambda (v: T).(clear x1 (CHead e (Bind
110 b) v))))) (\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop n O e (CHead
111 x0 (Flat f) t))))) (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind
112 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) (\lambda (x2: B).(\lambda (x3:
113 C).(\lambda (x4: T).(\lambda (H12: (clear x1 (CHead x3 (Bind x2)
114 x4))).(\lambda (H13: (drop n O x3 (CHead x0 (Flat f) t))).(let H14 \def
115 (csuba_clear_conf g x1 c2 H10 (CHead x3 (Bind x2) x4) H12) in (ex2_ind C
116 (\lambda (e2: C).(csuba g (CHead x3 (Bind x2) x4) e2)) (\lambda (e2:
117 C).(clear c2 e2)) (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind
118 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) (\lambda (x5: C).(\lambda (H15:
119 (csuba g (CHead x3 (Bind x2) x4) x5)).(\lambda (H16: (clear c2 x5)).(let H_x
120 \def (csuba_gen_bind g x2 x3 x5 x4 H15) in (let H17 \def H_x in (ex2_3_ind B
121 C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2: T).(eq C x5 (CHead e2
122 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g
123 x3 e2)))) (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind Abbr) u)))
124 (\lambda (d2: C).(csuba g d1 d2))) (\lambda (x6: B).(\lambda (x7: C).(\lambda
125 (x8: T).(\lambda (H18: (eq C x5 (CHead x7 (Bind x6) x8))).(\lambda (H19:
126 (csuba g x3 x7)).(let H20 \def (eq_ind C x5 (\lambda (c: C).(clear c2 c)) H16
127 (CHead x7 (Bind x6) x8) H18) in (let H21 \def (H8 x3 H13 x7 H19) in (ex2_ind
128 C (\lambda (d2: C).(getl n x7 (CHead d2 (Bind Abbr) u))) (\lambda (d2:
129 C).(csuba g d1 d2)) (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind
130 Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) (\lambda (x9: C).(\lambda (H22:
131 (getl n x7 (CHead x9 (Bind Abbr) u))).(\lambda (H23: (csuba g d1
132 x9)).(ex_intro2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind Abbr) u)))
133 (\lambda (d2: C).(csuba g d1 d2)) x9 (getl_clear_bind x6 c2 x7 x8 H20 (CHead
134 x9 (Bind Abbr) u) n H22) H23)))) H21)))))))) H17)))))) H14))))))) H11))))))))
135 i) H7))))) k H3 H4))))))) x H1 H2)))) H0))))))).
137 lemma csuba_getl_abst:
138 \forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).(\forall
139 (i: nat).((getl i c1 (CHead d1 (Bind Abst) u1)) \to (\forall (c2: C).((csuba
140 g c1 c2) \to (or (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst)
141 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
142 C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind Abbr) u2)))))
143 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
144 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
145 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
148 \lambda (g: G).(\lambda (c1: C).(\lambda (d1: C).(\lambda (u1: T).(\lambda
149 (i: nat).(\lambda (H: (getl i c1 (CHead d1 (Bind Abst) u1))).(let H0 \def
150 (getl_gen_all c1 (CHead d1 (Bind Abst) u1) i H) in (ex2_ind C (\lambda (e:
151 C).(drop i O c1 e)) (\lambda (e: C).(clear e (CHead d1 (Bind Abst) u1)))
152 (\forall (c2: C).((csuba g c1 c2) \to (or (ex2 C (\lambda (d2: C).(getl i c2
153 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
154 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind
155 Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1
156 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc
157 g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
158 a)))))))) (\lambda (x: C).(\lambda (H1: (drop i O c1 x)).(\lambda (H2: (clear
159 x (CHead d1 (Bind Abst) u1))).(C_ind (\lambda (c: C).((drop i O c1 c) \to
160 ((clear c (CHead d1 (Bind Abst) u1)) \to (\forall (c2: C).((csuba g c1 c2)
161 \to (or (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u1)))
162 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
163 (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind Abbr) u2))))) (\lambda
164 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
165 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
166 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))))))))) (\lambda
167 (n: nat).(\lambda (_: (drop i O c1 (CSort n))).(\lambda (H4: (clear (CSort n)
168 (CHead d1 (Bind Abst) u1))).(clear_gen_sort (CHead d1 (Bind Abst) u1) n H4
169 (\forall (c2: C).((csuba g c1 c2) \to (or (ex2 C (\lambda (d2: C).(getl i c2
170 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
171 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind
172 Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1
173 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc
174 g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
175 a)))))))))))) (\lambda (x0: C).(\lambda (_: (((drop i O c1 x0) \to ((clear x0
176 (CHead d1 (Bind Abst) u1)) \to (\forall (c2: C).((csuba g c1 c2) \to (or (ex2
177 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
178 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
179 (_: A).(getl i c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
180 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
181 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
182 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))))))))).(\lambda (k: K).(\lambda
183 (t: T).(\lambda (H3: (drop i O c1 (CHead x0 k t))).(\lambda (H4: (clear
184 (CHead x0 k t) (CHead d1 (Bind Abst) u1))).(K_ind (\lambda (k0: K).((drop i O
185 c1 (CHead x0 k0 t)) \to ((clear (CHead x0 k0 t) (CHead d1 (Bind Abst) u1))
186 \to (\forall (c2: C).((csuba g c1 c2) \to (or (ex2 C (\lambda (d2: C).(getl i
187 c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T
188 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2
189 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
190 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
191 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
192 u2 a))))))))))) (\lambda (b: B).(\lambda (H5: (drop i O c1 (CHead x0 (Bind b)
193 t))).(\lambda (H6: (clear (CHead x0 (Bind b) t) (CHead d1 (Bind Abst)
194 u1))).(let H7 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _)
195 \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1 (Bind Abst) u1)
196 (CHead x0 (Bind b) t) (clear_gen_bind b x0 (CHead d1 (Bind Abst) u1) t H6))
197 in ((let H8 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _)
198 \Rightarrow Abst | (CHead _ k0 _) \Rightarrow (match k0 with [(Bind b0)
199 \Rightarrow b0 | (Flat _) \Rightarrow Abst])])) (CHead d1 (Bind Abst) u1)
200 (CHead x0 (Bind b) t) (clear_gen_bind b x0 (CHead d1 (Bind Abst) u1) t H6))
201 in ((let H9 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _)
202 \Rightarrow u1 | (CHead _ _ t0) \Rightarrow t0])) (CHead d1 (Bind Abst) u1)
203 (CHead x0 (Bind b) t) (clear_gen_bind b x0 (CHead d1 (Bind Abst) u1) t H6))
204 in (\lambda (H10: (eq B Abst b)).(\lambda (H11: (eq C d1 x0)).(\lambda (c2:
205 C).(\lambda (H12: (csuba g c1 c2)).(let H13 \def (eq_ind_r T t (\lambda (t0:
206 T).(drop i O c1 (CHead x0 (Bind b) t0))) H5 u1 H9) in (let H14 \def (eq_ind_r
207 B b (\lambda (b0: B).(drop i O c1 (CHead x0 (Bind b0) u1))) H13 Abst H10) in
208 (let H15 \def (eq_ind_r C x0 (\lambda (c: C).(drop i O c1 (CHead c (Bind
209 Abst) u1))) H14 d1 H11) in (let H16 \def (csuba_drop_abst i c1 d1 u1 H15 g c2
210 H12) in (or_ind (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abst)
211 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
212 C).(\lambda (u2: T).(\lambda (_: A).(drop i O c2 (CHead d2 (Bind Abbr)
213 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
214 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
215 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
216 a))))) (or (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u1)))
217 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
218 (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind Abbr) u2))))) (\lambda
219 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
220 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
221 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda
222 (H17: (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abst) u1)))
223 (\lambda (d2: C).(csuba g d1 d2)))).(ex2_ind C (\lambda (d2: C).(drop i O c2
224 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) (or (ex2 C
225 (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
226 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
227 (_: A).(getl i c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
228 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
229 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
230 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x1: C).(\lambda
231 (H18: (drop i O c2 (CHead x1 (Bind Abst) u1))).(\lambda (H19: (csuba g d1
232 x1)).(or_introl (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst)
233 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
234 C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind Abbr) u2)))))
235 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
236 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
237 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))
238 (ex_intro2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u1))) (\lambda
239 (d2: C).(csuba g d1 d2)) x1 (getl_intro i c2 (CHead x1 (Bind Abst) u1) (CHead
240 x1 (Bind Abst) u1) H18 (clear_bind Abst x1 u1)) H19))))) H17)) (\lambda (H17:
241 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop i O c2
242 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
243 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
244 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
245 A).(arity g d2 u2 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2:
246 T).(\lambda (_: A).(drop i O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
247 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
248 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
249 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) (or (ex2 C
250 (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
251 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
252 (_: A).(getl i c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
253 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
254 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
255 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x1: C).(\lambda (x2:
256 T).(\lambda (x3: A).(\lambda (H18: (drop i O c2 (CHead x1 (Bind Abbr)
257 x2))).(\lambda (H19: (csuba g d1 x1)).(\lambda (H20: (arity g d1 u1 (asucc g
258 x3))).(\lambda (H21: (arity g x1 x2 x3)).(or_intror (ex2 C (\lambda (d2:
259 C).(getl i c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
260 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2
261 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
262 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
263 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
264 A).(arity g d2 u2 a))))) (ex4_3_intro C T A (\lambda (d2: C).(\lambda (u2:
265 T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
266 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
267 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
268 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) x1 x2 x3
269 (getl_intro i c2 (CHead x1 (Bind Abbr) x2) (CHead x1 (Bind Abbr) x2) H18
270 (clear_bind Abbr x1 x2)) H19 H20 H21))))))))) H17)) H16)))))))))) H8))
271 H7))))) (\lambda (f: F).(\lambda (H5: (drop i O c1 (CHead x0 (Flat f)
272 t))).(\lambda (H6: (clear (CHead x0 (Flat f) t) (CHead d1 (Bind Abst)
273 u1))).(let H7 \def H5 in (unintro C c1 (\lambda (c: C).((drop i O c (CHead x0
274 (Flat f) t)) \to (\forall (c2: C).((csuba g c c2) \to (or (ex2 C (\lambda
275 (d2: C).(getl i c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
276 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i
277 c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
278 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
279 A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
280 (a: A).(arity g d2 u2 a)))))))))) (nat_ind (\lambda (n: nat).(\forall (x1:
281 C).((drop n O x1 (CHead x0 (Flat f) t)) \to (\forall (c2: C).((csuba g x1 c2)
282 \to (or (ex2 C (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst) u1)))
283 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
284 (u2: T).(\lambda (_: A).(getl n c2 (CHead d2 (Bind Abbr) u2))))) (\lambda
285 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
286 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
287 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))))))))) (\lambda
288 (x1: C).(\lambda (H8: (drop O O x1 (CHead x0 (Flat f) t))).(\lambda (c2:
289 C).(\lambda (H9: (csuba g x1 c2)).(let H10 \def (eq_ind C x1 (\lambda (c:
290 C).(csuba g c c2)) H9 (CHead x0 (Flat f) t) (drop_gen_refl x1 (CHead x0 (Flat
291 f) t) H8)) in (let H_y \def (clear_flat x0 (CHead d1 (Bind Abst) u1)
292 (clear_gen_flat f x0 (CHead d1 (Bind Abst) u1) t H6) f t) in (let H11 \def
293 (csuba_clear_conf g (CHead x0 (Flat f) t) c2 H10 (CHead d1 (Bind Abst) u1)
294 H_y) in (ex2_ind C (\lambda (e2: C).(csuba g (CHead d1 (Bind Abst) u1) e2))
295 (\lambda (e2: C).(clear c2 e2)) (or (ex2 C (\lambda (d2: C).(getl O c2 (CHead
296 d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
297 (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl O c2 (CHead d2 (Bind Abbr)
298 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
299 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
300 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
301 a)))))) (\lambda (x2: C).(\lambda (H12: (csuba g (CHead d1 (Bind Abst) u1)
302 x2)).(\lambda (H13: (clear c2 x2)).(let H_x \def (csuba_gen_abst g d1 x2 u1
303 H12) in (let H14 \def H_x in (or_ind (ex2 C (\lambda (d2: C).(eq C x2 (CHead
304 d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda
305 (d2: C).(\lambda (u2: T).(\lambda (_: A).(eq C x2 (CHead d2 (Bind Abbr)
306 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
307 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
308 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
309 a))))) (or (ex2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abst) u1)))
310 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
311 (u2: T).(\lambda (_: A).(getl O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda
312 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
313 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
314 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda
315 (H15: (ex2 C (\lambda (d2: C).(eq C x2 (CHead d2 (Bind Abst) u1))) (\lambda
316 (d2: C).(csuba g d1 d2)))).(ex2_ind C (\lambda (d2: C).(eq C x2 (CHead d2
317 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) (or (ex2 C (\lambda (d2:
318 C).(getl O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
319 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl O c2
320 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
321 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
322 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
323 A).(arity g d2 u2 a)))))) (\lambda (x3: C).(\lambda (H16: (eq C x2 (CHead x3
324 (Bind Abst) u1))).(\lambda (H17: (csuba g d1 x3)).(let H18 \def (eq_ind C x2
325 (\lambda (c: C).(clear c2 c)) H13 (CHead x3 (Bind Abst) u1) H16) in
326 (or_introl (ex2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abst) u1)))
327 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
328 (u2: T).(\lambda (_: A).(getl O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda
329 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
330 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
331 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex_intro2 C
332 (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
333 C).(csuba g d1 d2)) x3 (getl_intro O c2 (CHead x3 (Bind Abst) u1) c2
334 (drop_refl c2) H18) H17)))))) H15)) (\lambda (H15: (ex4_3 C T A (\lambda (d2:
335 C).(\lambda (u2: T).(\lambda (_: A).(eq C x2 (CHead d2 (Bind Abbr) u2)))))
336 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
337 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
338 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
339 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
340 A).(eq C x2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
341 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
342 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
343 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) (or (ex2 C (\lambda (d2:
344 C).(getl O c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
345 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl O c2
346 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
347 A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
348 g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
349 A).(arity g d2 u2 a)))))) (\lambda (x3: C).(\lambda (x4: T).(\lambda (x5:
350 A).(\lambda (H16: (eq C x2 (CHead x3 (Bind Abbr) x4))).(\lambda (H17: (csuba
351 g d1 x3)).(\lambda (H18: (arity g d1 u1 (asucc g x5))).(\lambda (H19: (arity
352 g x3 x4 x5)).(let H20 \def (eq_ind C x2 (\lambda (c: C).(clear c2 c)) H13
353 (CHead x3 (Bind Abbr) x4) H16) in (or_intror (ex2 C (\lambda (d2: C).(getl O
354 c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T
355 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl O c2 (CHead d2
356 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
357 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
358 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
359 u2 a))))) (ex4_3_intro C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
360 A).(getl O c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
361 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
362 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
363 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) x3 x4 x5 (getl_intro O c2 (CHead
364 x3 (Bind Abbr) x4) c2 (drop_refl c2) H20) H17 H18 H19)))))))))) H15))
365 H14)))))) H11)))))))) (\lambda (n: nat).(\lambda (H8: ((\forall (x1:
366 C).((drop n O x1 (CHead x0 (Flat f) t)) \to (\forall (c2: C).((csuba g x1 c2)
367 \to (or (ex2 C (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst) u1)))
368 (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda
369 (u2: T).(\lambda (_: A).(getl n c2 (CHead d2 (Bind Abbr) u2))))) (\lambda
370 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
371 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
372 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
373 a)))))))))))).(\lambda (x1: C).(\lambda (H9: (drop (S n) O x1 (CHead x0 (Flat
374 f) t))).(\lambda (c2: C).(\lambda (H10: (csuba g x1 c2)).(let H11 \def
375 (drop_clear x1 (CHead x0 (Flat f) t) n H9) in (ex2_3_ind B C T (\lambda (b:
376 B).(\lambda (e: C).(\lambda (v: T).(clear x1 (CHead e (Bind b) v)))))
377 (\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop n O e (CHead x0 (Flat
378 f) t))))) (or (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind Abst)
379 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
380 C).(\lambda (u2: T).(\lambda (_: A).(getl (S n) c2 (CHead d2 (Bind Abbr)
381 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
382 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
383 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
384 a)))))) (\lambda (x2: B).(\lambda (x3: C).(\lambda (x4: T).(\lambda (H12:
385 (clear x1 (CHead x3 (Bind x2) x4))).(\lambda (H13: (drop n O x3 (CHead x0
386 (Flat f) t))).(let H14 \def (csuba_clear_conf g x1 c2 H10 (CHead x3 (Bind x2)
387 x4) H12) in (ex2_ind C (\lambda (e2: C).(csuba g (CHead x3 (Bind x2) x4) e2))
388 (\lambda (e2: C).(clear c2 e2)) (or (ex2 C (\lambda (d2: C).(getl (S n) c2
389 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A
390 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl (S n) c2 (CHead d2
391 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
392 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
393 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
394 u2 a)))))) (\lambda (x5: C).(\lambda (H15: (csuba g (CHead x3 (Bind x2) x4)
395 x5)).(\lambda (H16: (clear c2 x5)).(let H_x \def (csuba_gen_bind g x2 x3 x5
396 x4 H15) in (let H17 \def H_x in (ex2_3_ind B C T (\lambda (b2: B).(\lambda
397 (e2: C).(\lambda (v2: T).(eq C x5 (CHead e2 (Bind b2) v2))))) (\lambda (_:
398 B).(\lambda (e2: C).(\lambda (_: T).(csuba g x3 e2)))) (or (ex2 C (\lambda
399 (d2: C).(getl (S n) c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g
400 d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl
401 (S n) c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
402 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
403 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
404 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda (x6: B).(\lambda (x7:
405 C).(\lambda (x8: T).(\lambda (H18: (eq C x5 (CHead x7 (Bind x6)
406 x8))).(\lambda (H19: (csuba g x3 x7)).(let H20 \def (eq_ind C x5 (\lambda (c:
407 C).(clear c2 c)) H16 (CHead x7 (Bind x6) x8) H18) in (let H21 \def (H8 x3 H13
408 x7 H19) in (or_ind (ex2 C (\lambda (d2: C).(getl n x7 (CHead d2 (Bind Abst)
409 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
410 C).(\lambda (u2: T).(\lambda (_: A).(getl n x7 (CHead d2 (Bind Abbr) u2)))))
411 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
412 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
413 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (or
414 (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind Abst) u1))) (\lambda
415 (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
416 T).(\lambda (_: A).(getl (S n) c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
417 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
418 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
419 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))) (\lambda
420 (H22: (ex2 C (\lambda (d2: C).(getl n x7 (CHead d2 (Bind Abst) u1))) (\lambda
421 (d2: C).(csuba g d1 d2)))).(ex2_ind C (\lambda (d2: C).(getl n x7 (CHead d2
422 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)) (or (ex2 C (\lambda (d2:
423 C).(getl (S n) c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
424 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl (S
425 n) c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
426 (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a:
427 A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda
428 (a: A).(arity g d2 u2 a)))))) (\lambda (x9: C).(\lambda (H23: (getl n x7
429 (CHead x9 (Bind Abst) u1))).(\lambda (H24: (csuba g d1 x9)).(or_introl (ex2 C
430 (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
431 C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
432 (_: A).(getl (S n) c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda
433 (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
434 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
435 (u2: T).(\lambda (a: A).(arity g d2 u2 a))))) (ex_intro2 C (\lambda (d2:
436 C).(getl (S n) c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1
437 d2)) x9 (getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind Abst) u1) n H23)
438 H24))))) H22)) (\lambda (H22: (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
439 T).(\lambda (_: A).(getl n x7 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2:
440 C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_:
441 C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda
442 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))).(ex4_3_ind C
443 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl n x7 (CHead d2
444 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
445 d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
446 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2
447 u2 a)))) (or (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind Abst)
448 u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
449 C).(\lambda (u2: T).(\lambda (_: A).(getl (S n) c2 (CHead d2 (Bind Abbr)
450 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
451 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
452 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
453 a)))))) (\lambda (x9: C).(\lambda (x10: T).(\lambda (x11: A).(\lambda (H23:
454 (getl n x7 (CHead x9 (Bind Abbr) x10))).(\lambda (H24: (csuba g d1
455 x9)).(\lambda (H25: (arity g d1 u1 (asucc g x11))).(\lambda (H26: (arity g x9
456 x10 x11)).(or_intror (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind
457 Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
458 C).(\lambda (u2: T).(\lambda (_: A).(getl (S n) c2 (CHead d2 (Bind Abbr)
459 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
460 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
461 a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
462 a))))) (ex4_3_intro C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
463 A).(getl (S n) c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
464 T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
465 T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
466 (u2: T).(\lambda (a: A).(arity g d2 u2 a)))) x9 x10 x11 (getl_clear_bind x6
467 c2 x7 x8 H20 (CHead x9 (Bind Abbr) x10) n H23) H24 H25 H26))))))))) H22))
468 H21)))))))) H17)))))) H14))))))) H11)))))))) i) H7))))) k H3 H4))))))) x H1
471 lemma csuba_getl_abst_rev:
472 \forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall
473 (i: nat).((getl i c1 (CHead d1 (Bind Abst) u)) \to (\forall (c2: C).((csuba g
474 c2 c1) \to (or (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u)))
475 (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
476 T).(getl i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
477 T).(csuba g d2 d1))))))))))))
479 \lambda (g: G).(\lambda (c1: C).(\lambda (d1: C).(\lambda (u: T).(\lambda
480 (i: nat).(\lambda (H: (getl i c1 (CHead d1 (Bind Abst) u))).(let H0 \def
481 (getl_gen_all c1 (CHead d1 (Bind Abst) u) i H) in (ex2_ind C (\lambda (e:
482 C).(drop i O c1 e)) (\lambda (e: C).(clear e (CHead d1 (Bind Abst) u)))
483 (\forall (c2: C).((csuba g c2 c1) \to (or (ex2 C (\lambda (d2: C).(getl i c2
484 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
485 (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2))))
486 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))) (\lambda (x:
487 C).(\lambda (H1: (drop i O c1 x)).(\lambda (H2: (clear x (CHead d1 (Bind
488 Abst) u))).(C_ind (\lambda (c: C).((drop i O c1 c) \to ((clear c (CHead d1
489 (Bind Abst) u)) \to (\forall (c2: C).((csuba g c2 c1) \to (or (ex2 C (\lambda
490 (d2: C).(getl i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
491 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind
492 Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))))))
493 (\lambda (n: nat).(\lambda (_: (drop i O c1 (CSort n))).(\lambda (H4: (clear
494 (CSort n) (CHead d1 (Bind Abst) u))).(clear_gen_sort (CHead d1 (Bind Abst) u)
495 n H4 (\forall (c2: C).((csuba g c2 c1) \to (or (ex2 C (\lambda (d2: C).(getl
496 i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
497 (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2))))
498 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))))))) (\lambda (x0:
499 C).(\lambda (_: (((drop i O c1 x0) \to ((clear x0 (CHead d1 (Bind Abst) u))
500 \to (\forall (c2: C).((csuba g c2 c1) \to (or (ex2 C (\lambda (d2: C).(getl i
501 c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
502 (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2))))
503 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))))))).(\lambda (k:
504 K).(\lambda (t: T).(\lambda (H3: (drop i O c1 (CHead x0 k t))).(\lambda (H4:
505 (clear (CHead x0 k t) (CHead d1 (Bind Abst) u))).(K_ind (\lambda (k0:
506 K).((drop i O c1 (CHead x0 k0 t)) \to ((clear (CHead x0 k0 t) (CHead d1 (Bind
507 Abst) u)) \to (\forall (c2: C).((csuba g c2 c1) \to (or (ex2 C (\lambda (d2:
508 C).(getl i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))
509 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void)
510 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))))))) (\lambda (b:
511 B).(\lambda (H5: (drop i O c1 (CHead x0 (Bind b) t))).(\lambda (H6: (clear
512 (CHead x0 (Bind b) t) (CHead d1 (Bind Abst) u))).(let H7 \def (f_equal C C
513 (\lambda (e: C).(match e with [(CSort _) \Rightarrow d1 | (CHead c _ _)
514 \Rightarrow c])) (CHead d1 (Bind Abst) u) (CHead x0 (Bind b) t)
515 (clear_gen_bind b x0 (CHead d1 (Bind Abst) u) t H6)) in ((let H8 \def
516 (f_equal C B (\lambda (e: C).(match e with [(CSort _) \Rightarrow Abst |
517 (CHead _ k0 _) \Rightarrow (match k0 with [(Bind b0) \Rightarrow b0 | (Flat
518 _) \Rightarrow Abst])])) (CHead d1 (Bind Abst) u) (CHead x0 (Bind b) t)
519 (clear_gen_bind b x0 (CHead d1 (Bind Abst) u) t H6)) in ((let H9 \def
520 (f_equal C T (\lambda (e: C).(match e with [(CSort _) \Rightarrow u | (CHead
521 _ _ t0) \Rightarrow t0])) (CHead d1 (Bind Abst) u) (CHead x0 (Bind b) t)
522 (clear_gen_bind b x0 (CHead d1 (Bind Abst) u) t H6)) in (\lambda (H10: (eq B
523 Abst b)).(\lambda (H11: (eq C d1 x0)).(\lambda (c2: C).(\lambda (H12: (csuba
524 g c2 c1)).(let H13 \def (eq_ind_r T t (\lambda (t0: T).(drop i O c1 (CHead x0
525 (Bind b) t0))) H5 u H9) in (let H14 \def (eq_ind_r B b (\lambda (b0: B).(drop
526 i O c1 (CHead x0 (Bind b0) u))) H13 Abst H10) in (let H15 \def (eq_ind_r C x0
527 (\lambda (c: C).(drop i O c1 (CHead c (Bind Abst) u))) H14 d1 H11) in (let
528 H16 \def (csuba_drop_abst_rev i c1 d1 u H15 g c2 H12) in (or_ind (ex2 C
529 (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
530 C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(drop i O
531 c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
532 d1)))) (or (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u)))
533 (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
534 T).(getl i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
535 T).(csuba g d2 d1))))) (\lambda (H17: (ex2 C (\lambda (d2: C).(drop i O c2
536 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))).(ex2_ind C
537 (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
538 C).(csuba g d2 d1)) (or (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind
539 Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2:
540 C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2:
541 C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (x1: C).(\lambda (H18: (drop
542 i O c2 (CHead x1 (Bind Abst) u))).(\lambda (H19: (csuba g x1 d1)).(or_introl
543 (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
544 C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl i c2
545 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
546 d1)))) (ex_intro2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u)))
547 (\lambda (d2: C).(csuba g d2 d1)) x1 (getl_intro i c2 (CHead x1 (Bind Abst)
548 u) (CHead x1 (Bind Abst) u) H18 (clear_bind Abst x1 u)) H19))))) H17))
549 (\lambda (H17: (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(drop i O c2
550 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
551 d1))))).(ex2_2_ind C T (\lambda (d2: C).(\lambda (u2: T).(drop i O c2 (CHead
552 d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))) (or
553 (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
554 C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl i c2
555 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
556 d1))))) (\lambda (x1: C).(\lambda (x2: T).(\lambda (H18: (drop i O c2 (CHead
557 x1 (Bind Void) x2))).(\lambda (H19: (csuba g x1 d1)).(or_intror (ex2 C
558 (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
559 C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl i c2
560 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
561 d1)))) (ex2_2_intro C T (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead
562 d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))) x1
563 x2 (getl_intro i c2 (CHead x1 (Bind Void) x2) (CHead x1 (Bind Void) x2) H18
564 (clear_bind Void x1 x2)) H19)))))) H17)) H16)))))))))) H8)) H7))))) (\lambda
565 (f: F).(\lambda (H5: (drop i O c1 (CHead x0 (Flat f) t))).(\lambda (H6:
566 (clear (CHead x0 (Flat f) t) (CHead d1 (Bind Abst) u))).(let H7 \def H5 in
567 (unintro C c1 (\lambda (c: C).((drop i O c (CHead x0 (Flat f) t)) \to
568 (\forall (c2: C).((csuba g c2 c) \to (or (ex2 C (\lambda (d2: C).(getl i c2
569 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
570 (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2))))
571 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))))) (nat_ind (\lambda
572 (n: nat).(\forall (x1: C).((drop n O x1 (CHead x0 (Flat f) t)) \to (\forall
573 (c2: C).((csuba g c2 x1) \to (or (ex2 C (\lambda (d2: C).(getl n c2 (CHead d2
574 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2:
575 C).(\lambda (u2: T).(getl n c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2:
576 C).(\lambda (_: T).(csuba g d2 d1)))))))))) (\lambda (x1: C).(\lambda (H8:
577 (drop O O x1 (CHead x0 (Flat f) t))).(\lambda (c2: C).(\lambda (H9: (csuba g
578 c2 x1)).(let H10 \def (eq_ind C x1 (\lambda (c: C).(csuba g c2 c)) H9 (CHead
579 x0 (Flat f) t) (drop_gen_refl x1 (CHead x0 (Flat f) t) H8)) in (let H_y \def
580 (clear_flat x0 (CHead d1 (Bind Abst) u) (clear_gen_flat f x0 (CHead d1 (Bind
581 Abst) u) t H6) f t) in (let H11 \def (csuba_clear_trans g (CHead x0 (Flat f)
582 t) c2 H10 (CHead d1 (Bind Abst) u) H_y) in (ex2_ind C (\lambda (e2: C).(csuba
583 g e2 (CHead d1 (Bind Abst) u))) (\lambda (e2: C).(clear c2 e2)) (or (ex2 C
584 (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
585 C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl O c2
586 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
587 d1))))) (\lambda (x2: C).(\lambda (H12: (csuba g x2 (CHead d1 (Bind Abst)
588 u))).(\lambda (H13: (clear c2 x2)).(let H_x \def (csuba_gen_abst_rev g d1 x2
589 u H12) in (let H14 \def H_x in (or_ind (ex2 C (\lambda (d2: C).(eq C x2
590 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
591 (\lambda (d2: C).(\lambda (u2: T).(eq C x2 (CHead d2 (Bind Void) u2))))
592 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))) (or (ex2 C (\lambda (d2:
593 C).(getl O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))
594 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl O c2 (CHead d2 (Bind Void)
595 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (H15:
596 (ex2 C (\lambda (d2: C).(eq C x2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
597 C).(csuba g d2 d1)))).(ex2_ind C (\lambda (d2: C).(eq C x2 (CHead d2 (Bind
598 Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) (or (ex2 C (\lambda (d2:
599 C).(getl O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1)))
600 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl O c2 (CHead d2 (Bind Void)
601 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (x3:
602 C).(\lambda (H16: (eq C x2 (CHead x3 (Bind Abst) u))).(\lambda (H17: (csuba g
603 x3 d1)).(let H18 \def (eq_ind C x2 (\lambda (c: C).(clear c2 c)) H13 (CHead
604 x3 (Bind Abst) u) H16) in (or_introl (ex2 C (\lambda (d2: C).(getl O c2
605 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
606 (\lambda (d2: C).(\lambda (u2: T).(getl O c2 (CHead d2 (Bind Void) u2))))
607 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))) (ex_intro2 C (\lambda
608 (d2: C).(getl O c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
609 d1)) x3 (getl_intro O c2 (CHead x3 (Bind Abst) u) c2 (drop_refl c2) H18)
610 H17)))))) H15)) (\lambda (H15: (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
611 T).(eq C x2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
612 T).(csuba g d2 d1))))).(ex2_2_ind C T (\lambda (d2: C).(\lambda (u2: T).(eq C
613 x2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
614 d1))) (or (ex2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abst) u)))
615 (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
616 T).(getl O c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
617 T).(csuba g d2 d1))))) (\lambda (x3: C).(\lambda (x4: T).(\lambda (H16: (eq C
618 x2 (CHead x3 (Bind Void) x4))).(\lambda (H17: (csuba g x3 d1)).(let H18 \def
619 (eq_ind C x2 (\lambda (c: C).(clear c2 c)) H13 (CHead x3 (Bind Void) x4) H16)
620 in (or_intror (ex2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abst) u)))
621 (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
622 T).(getl O c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
623 T).(csuba g d2 d1)))) (ex2_2_intro C T (\lambda (d2: C).(\lambda (u2:
624 T).(getl O c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
625 T).(csuba g d2 d1))) x3 x4 (getl_intro O c2 (CHead x3 (Bind Void) x4) c2
626 (drop_refl c2) H18) H17))))))) H15)) H14)))))) H11)))))))) (\lambda (n:
627 nat).(\lambda (H8: ((\forall (x1: C).((drop n O x1 (CHead x0 (Flat f) t)) \to
628 (\forall (c2: C).((csuba g c2 x1) \to (or (ex2 C (\lambda (d2: C).(getl n c2
629 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
630 (\lambda (d2: C).(\lambda (u2: T).(getl n c2 (CHead d2 (Bind Void) u2))))
631 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))))))).(\lambda (x1:
632 C).(\lambda (H9: (drop (S n) O x1 (CHead x0 (Flat f) t))).(\lambda (c2:
633 C).(\lambda (H10: (csuba g c2 x1)).(let H11 \def (drop_clear x1 (CHead x0
634 (Flat f) t) n H9) in (ex2_3_ind B C T (\lambda (b: B).(\lambda (e:
635 C).(\lambda (v: T).(clear x1 (CHead e (Bind b) v))))) (\lambda (_:
636 B).(\lambda (e: C).(\lambda (_: T).(drop n O e (CHead x0 (Flat f) t))))) (or
637 (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind Abst) u))) (\lambda
638 (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl
639 (S n) c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba
640 g d2 d1))))) (\lambda (x2: B).(\lambda (x3: C).(\lambda (x4: T).(\lambda
641 (H12: (clear x1 (CHead x3 (Bind x2) x4))).(\lambda (H13: (drop n O x3 (CHead
642 x0 (Flat f) t))).(let H14 \def (csuba_clear_trans g x1 c2 H10 (CHead x3 (Bind
643 x2) x4) H12) in (ex2_ind C (\lambda (e2: C).(csuba g e2 (CHead x3 (Bind x2)
644 x4))) (\lambda (e2: C).(clear c2 e2)) (or (ex2 C (\lambda (d2: C).(getl (S n)
645 c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
646 (\lambda (d2: C).(\lambda (u2: T).(getl (S n) c2 (CHead d2 (Bind Void) u2))))
647 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (x5:
648 C).(\lambda (H15: (csuba g x5 (CHead x3 (Bind x2) x4))).(\lambda (H16: (clear
649 c2 x5)).(let H_x \def (csuba_gen_bind_rev g x2 x3 x5 x4 H15) in (let H17 \def
650 H_x in (ex2_3_ind B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda (v2:
651 T).(eq C x5 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
652 C).(\lambda (_: T).(csuba g e2 x3)))) (or (ex2 C (\lambda (d2: C).(getl (S n)
653 c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
654 (\lambda (d2: C).(\lambda (u2: T).(getl (S n) c2 (CHead d2 (Bind Void) u2))))
655 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (x6:
656 B).(\lambda (x7: C).(\lambda (x8: T).(\lambda (H18: (eq C x5 (CHead x7 (Bind
657 x6) x8))).(\lambda (H19: (csuba g x7 x3)).(let H20 \def (eq_ind C x5 (\lambda
658 (c: C).(clear c2 c)) H16 (CHead x7 (Bind x6) x8) H18) in (let H21 \def (H8 x3
659 H13 x7 H19) in (or_ind (ex2 C (\lambda (d2: C).(getl n x7 (CHead d2 (Bind
660 Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2:
661 C).(\lambda (u2: T).(getl n x7 (CHead d2 (Bind Void) u2)))) (\lambda (d2:
662 C).(\lambda (_: T).(csuba g d2 d1)))) (or (ex2 C (\lambda (d2: C).(getl (S n)
663 c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T
664 (\lambda (d2: C).(\lambda (u2: T).(getl (S n) c2 (CHead d2 (Bind Void) u2))))
665 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (H22: (ex2 C
666 (\lambda (d2: C).(getl n x7 (CHead d2 (Bind Abst) u))) (\lambda (d2:
667 C).(csuba g d2 d1)))).(ex2_ind C (\lambda (d2: C).(getl n x7 (CHead d2 (Bind
668 Abst) u))) (\lambda (d2: C).(csuba g d2 d1)) (or (ex2 C (\lambda (d2:
669 C).(getl (S n) c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
670 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl (S n) c2 (CHead d2
671 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))
672 (\lambda (x9: C).(\lambda (H23: (getl n x7 (CHead x9 (Bind Abst)
673 u))).(\lambda (H24: (csuba g x9 d1)).(or_introl (ex2 C (\lambda (d2: C).(getl
674 (S n) c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2
675 C T (\lambda (d2: C).(\lambda (u2: T).(getl (S n) c2 (CHead d2 (Bind Void)
676 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))) (ex_intro2 C
677 (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind Abst) u))) (\lambda (d2:
678 C).(csuba g d2 d1)) x9 (getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind Abst)
679 u) n H23) H24))))) H22)) (\lambda (H22: (ex2_2 C T (\lambda (d2: C).(\lambda
680 (u2: T).(getl n x7 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
681 T).(csuba g d2 d1))))).(ex2_2_ind C T (\lambda (d2: C).(\lambda (u2: T).(getl
682 n x7 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g
683 d2 d1))) (or (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind Abst)
684 u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda
685 (u2: T).(getl (S n) c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda
686 (_: T).(csuba g d2 d1))))) (\lambda (x9: C).(\lambda (x10: T).(\lambda (H23:
687 (getl n x7 (CHead x9 (Bind Void) x10))).(\lambda (H24: (csuba g x9
688 d1)).(or_intror (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind Abst)
689 u))) (\lambda (d2: C).(csuba g d2 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda
690 (u2: T).(getl (S n) c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda
691 (_: T).(csuba g d2 d1)))) (ex2_2_intro C T (\lambda (d2: C).(\lambda (u2:
692 T).(getl (S n) c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
693 T).(csuba g d2 d1))) x9 x10 (getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind
694 Void) x10) n H23) H24)))))) H22)) H21)))))))) H17)))))) H14)))))))
695 H11)))))))) i) H7))))) k H3 H4))))))) x H1 H2)))) H0))))))).
697 lemma csuba_getl_abbr_rev:
698 \forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).(\forall
699 (i: nat).((getl i c1 (CHead d1 (Bind Abbr) u1)) \to (\forall (c2: C).((csuba
700 g c2 c1) \to (or3 (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abbr)
701 u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
702 C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind Abst) u2)))))
703 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
704 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
705 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex2_2
706 C T (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2))))
707 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))))))))
709 \lambda (g: G).(\lambda (c1: C).(\lambda (d1: C).(\lambda (u1: T).(\lambda
710 (i: nat).(\lambda (H: (getl i c1 (CHead d1 (Bind Abbr) u1))).(let H0 \def
711 (getl_gen_all c1 (CHead d1 (Bind Abbr) u1) i H) in (ex2_ind C (\lambda (e:
712 C).(drop i O c1 e)) (\lambda (e: C).(clear e (CHead d1 (Bind Abbr) u1)))
713 (\forall (c2: C).((csuba g c2 c1) \to (or3 (ex2 C (\lambda (d2: C).(getl i c2
714 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A
715 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind
716 Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2
717 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
718 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
719 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2
720 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))))
721 (\lambda (x: C).(\lambda (H1: (drop i O c1 x)).(\lambda (H2: (clear x (CHead
722 d1 (Bind Abbr) u1))).(C_ind (\lambda (c: C).((drop i O c1 c) \to ((clear c
723 (CHead d1 (Bind Abbr) u1)) \to (\forall (c2: C).((csuba g c2 c1) \to (or3
724 (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
725 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
726 (_: A).(getl i c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
727 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
728 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
729 (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2:
730 C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2:
731 C).(\lambda (_: T).(csuba g d2 d1)))))))))) (\lambda (n: nat).(\lambda (_:
732 (drop i O c1 (CSort n))).(\lambda (H4: (clear (CSort n) (CHead d1 (Bind Abbr)
733 u1))).(clear_gen_sort (CHead d1 (Bind Abbr) u1) n H4 (\forall (c2: C).((csuba
734 g c2 c1) \to (or3 (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abbr)
735 u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
736 C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind Abst) u2)))))
737 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
738 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
739 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex2_2
740 C T (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2))))
741 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))))))))) (\lambda (x0:
742 C).(\lambda (_: (((drop i O c1 x0) \to ((clear x0 (CHead d1 (Bind Abbr) u1))
743 \to (\forall (c2: C).((csuba g c2 c1) \to (or3 (ex2 C (\lambda (d2: C).(getl
744 i c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C
745 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2
746 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
747 d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
748 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
749 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2
750 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2
751 d1))))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (H3: (drop i O c1
752 (CHead x0 k t))).(\lambda (H4: (clear (CHead x0 k t) (CHead d1 (Bind Abbr)
753 u1))).(K_ind (\lambda (k0: K).((drop i O c1 (CHead x0 k0 t)) \to ((clear
754 (CHead x0 k0 t) (CHead d1 (Bind Abbr) u1)) \to (\forall (c2: C).((csuba g c2
755 c1) \to (or3 (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abbr) u1)))
756 (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda
757 (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind Abst) u2))))) (\lambda
758 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
759 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
760 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex2_2 C T
761 (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2))))
762 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))))))) (\lambda (b:
763 B).(\lambda (H5: (drop i O c1 (CHead x0 (Bind b) t))).(\lambda (H6: (clear
764 (CHead x0 (Bind b) t) (CHead d1 (Bind Abbr) u1))).(let H7 \def (f_equal C C
765 (\lambda (e: C).(match e with [(CSort _) \Rightarrow d1 | (CHead c _ _)
766 \Rightarrow c])) (CHead d1 (Bind Abbr) u1) (CHead x0 (Bind b) t)
767 (clear_gen_bind b x0 (CHead d1 (Bind Abbr) u1) t H6)) in ((let H8 \def
768 (f_equal C B (\lambda (e: C).(match e with [(CSort _) \Rightarrow Abbr |
769 (CHead _ k0 _) \Rightarrow (match k0 with [(Bind b0) \Rightarrow b0 | (Flat
770 _) \Rightarrow Abbr])])) (CHead d1 (Bind Abbr) u1) (CHead x0 (Bind b) t)
771 (clear_gen_bind b x0 (CHead d1 (Bind Abbr) u1) t H6)) in ((let H9 \def
772 (f_equal C T (\lambda (e: C).(match e with [(CSort _) \Rightarrow u1 | (CHead
773 _ _ t0) \Rightarrow t0])) (CHead d1 (Bind Abbr) u1) (CHead x0 (Bind b) t)
774 (clear_gen_bind b x0 (CHead d1 (Bind Abbr) u1) t H6)) in (\lambda (H10: (eq B
775 Abbr b)).(\lambda (H11: (eq C d1 x0)).(\lambda (c2: C).(\lambda (H12: (csuba
776 g c2 c1)).(let H13 \def (eq_ind_r T t (\lambda (t0: T).(drop i O c1 (CHead x0
777 (Bind b) t0))) H5 u1 H9) in (let H14 \def (eq_ind_r B b (\lambda (b0:
778 B).(drop i O c1 (CHead x0 (Bind b0) u1))) H13 Abbr H10) in (let H15 \def
779 (eq_ind_r C x0 (\lambda (c: C).(drop i O c1 (CHead c (Bind Abbr) u1))) H14 d1
780 H11) in (let H16 \def (csuba_drop_abbr_rev i c1 d1 u1 H15 g c2 H12) in
781 (or3_ind (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abbr) u1)))
782 (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda
783 (u2: T).(\lambda (_: A).(drop i O c2 (CHead d2 (Bind Abst) u2))))) (\lambda
784 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
785 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
786 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex2_2 C T
787 (\lambda (d2: C).(\lambda (u2: T).(drop i O c2 (CHead d2 (Bind Void) u2))))
788 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))) (or3 (ex2 C (\lambda (d2:
789 C).(getl i c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))
790 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2
791 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
792 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
793 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
794 (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
795 T).(getl i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
796 T).(csuba g d2 d1))))) (\lambda (H17: (ex2 C (\lambda (d2: C).(drop i O c2
797 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))).(ex2_ind C
798 (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
799 C).(csuba g d2 d1)) (or3 (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind
800 Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
801 C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind Abst) u2)))))
802 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
803 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
804 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex2_2
805 C T (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2))))
806 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (x1:
807 C).(\lambda (H18: (drop i O c2 (CHead x1 (Bind Abbr) u1))).(\lambda (H19:
808 (csuba g x1 d1)).(or3_intro0 (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2
809 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
810 (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind Abst)
811 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
812 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
813 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
814 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void)
815 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))) (ex_intro2 C
816 (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
817 C).(csuba g d2 d1)) x1 (getl_intro i c2 (CHead x1 (Bind Abbr) u1) (CHead x1
818 (Bind Abbr) u1) H18 (clear_bind Abbr x1 u1)) H19))))) H17)) (\lambda (H17:
819 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(drop i O c2
820 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
821 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
822 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
823 (a: A).(arity g d1 u1 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2:
824 T).(\lambda (_: A).(drop i O c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
825 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
826 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
827 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))) (or3 (ex2 C
828 (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
829 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
830 (_: A).(getl i c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
831 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
832 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
833 (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2:
834 C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2:
835 C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (x1: C).(\lambda (x2:
836 T).(\lambda (x3: A).(\lambda (H18: (drop i O c2 (CHead x1 (Bind Abst)
837 x2))).(\lambda (H19: (csuba g x1 d1)).(\lambda (H20: (arity g x1 x2 (asucc g
838 x3))).(\lambda (H21: (arity g d1 u1 x3)).(or3_intro1 (ex2 C (\lambda (d2:
839 C).(getl i c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))
840 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2
841 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
842 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
843 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
844 (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
845 T).(getl i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
846 T).(csuba g d2 d1)))) (ex4_3_intro C T A (\lambda (d2: C).(\lambda (u2:
847 T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
848 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
849 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
850 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))) x1 x2 x3
851 (getl_intro i c2 (CHead x1 (Bind Abst) x2) (CHead x1 (Bind Abst) x2) H18
852 (clear_bind Abst x1 x2)) H19 H20 H21))))))))) H17)) (\lambda (H17: (ex2_2 C T
853 (\lambda (d2: C).(\lambda (u2: T).(drop i O c2 (CHead d2 (Bind Void) u2))))
854 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))).(ex2_2_ind C T (\lambda
855 (d2: C).(\lambda (u2: T).(drop i O c2 (CHead d2 (Bind Void) u2)))) (\lambda
856 (d2: C).(\lambda (_: T).(csuba g d2 d1))) (or3 (ex2 C (\lambda (d2: C).(getl
857 i c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C
858 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2
859 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
860 d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
861 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
862 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2
863 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))
864 (\lambda (x1: C).(\lambda (x2: T).(\lambda (H18: (drop i O c2 (CHead x1 (Bind
865 Void) x2))).(\lambda (H19: (csuba g x1 d1)).(or3_intro2 (ex2 C (\lambda (d2:
866 C).(getl i c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))
867 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2
868 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
869 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
870 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
871 (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
872 T).(getl i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
873 T).(csuba g d2 d1)))) (ex2_2_intro C T (\lambda (d2: C).(\lambda (u2:
874 T).(getl i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
875 T).(csuba g d2 d1))) x1 x2 (getl_intro i c2 (CHead x1 (Bind Void) x2) (CHead
876 x1 (Bind Void) x2) H18 (clear_bind Void x1 x2)) H19)))))) H17)) H16))))))))))
877 H8)) H7))))) (\lambda (f: F).(\lambda (H5: (drop i O c1 (CHead x0 (Flat f)
878 t))).(\lambda (H6: (clear (CHead x0 (Flat f) t) (CHead d1 (Bind Abbr)
879 u1))).(let H7 \def H5 in (unintro C c1 (\lambda (c: C).((drop i O c (CHead x0
880 (Flat f) t)) \to (\forall (c2: C).((csuba g c2 c) \to (or3 (ex2 C (\lambda
881 (d2: C).(getl i c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
882 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i
883 c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
884 (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
885 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
886 (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
887 T).(getl i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
888 T).(csuba g d2 d1))))))))) (nat_ind (\lambda (n: nat).(\forall (x1: C).((drop
889 n O x1 (CHead x0 (Flat f) t)) \to (\forall (c2: C).((csuba g c2 x1) \to (or3
890 (ex2 C (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
891 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
892 (_: A).(getl n c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
893 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
894 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
895 (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2:
896 C).(\lambda (u2: T).(getl n c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2:
897 C).(\lambda (_: T).(csuba g d2 d1)))))))))) (\lambda (x1: C).(\lambda (H8:
898 (drop O O x1 (CHead x0 (Flat f) t))).(\lambda (c2: C).(\lambda (H9: (csuba g
899 c2 x1)).(let H10 \def (eq_ind C x1 (\lambda (c: C).(csuba g c2 c)) H9 (CHead
900 x0 (Flat f) t) (drop_gen_refl x1 (CHead x0 (Flat f) t) H8)) in (let H_y \def
901 (clear_flat x0 (CHead d1 (Bind Abbr) u1) (clear_gen_flat f x0 (CHead d1 (Bind
902 Abbr) u1) t H6) f t) in (let H11 \def (csuba_clear_trans g (CHead x0 (Flat f)
903 t) c2 H10 (CHead d1 (Bind Abbr) u1) H_y) in (ex2_ind C (\lambda (e2:
904 C).(csuba g e2 (CHead d1 (Bind Abbr) u1))) (\lambda (e2: C).(clear c2 e2))
905 (or3 (ex2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abbr) u1))) (\lambda
906 (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2:
907 T).(\lambda (_: A).(getl O c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2:
908 C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
909 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
910 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex2_2 C T
911 (\lambda (d2: C).(\lambda (u2: T).(getl O c2 (CHead d2 (Bind Void) u2))))
912 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (x2:
913 C).(\lambda (H12: (csuba g x2 (CHead d1 (Bind Abbr) u1))).(\lambda (H13:
914 (clear c2 x2)).(let H_x \def (csuba_gen_abbr_rev g d1 x2 u1 H12) in (let H14
915 \def H_x in (or3_ind (ex2 C (\lambda (d2: C).(eq C x2 (CHead d2 (Bind Abbr)
916 u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
917 C).(\lambda (u2: T).(\lambda (_: A).(eq C x2 (CHead d2 (Bind Abst) u2)))))
918 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
919 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
920 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex2_2
921 C T (\lambda (d2: C).(\lambda (u2: T).(eq C x2 (CHead d2 (Bind Void) u2))))
922 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))) (or3 (ex2 C (\lambda (d2:
923 C).(getl O c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))
924 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl O c2
925 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
926 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
927 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
928 (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
929 T).(getl O c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
930 T).(csuba g d2 d1))))) (\lambda (H15: (ex2 C (\lambda (d2: C).(eq C x2 (CHead
931 d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))).(ex2_ind C (\lambda
932 (d2: C).(eq C x2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
933 d1)) (or3 (ex2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abbr) u1)))
934 (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda
935 (u2: T).(\lambda (_: A).(getl O c2 (CHead d2 (Bind Abst) u2))))) (\lambda
936 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
937 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
938 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex2_2 C T
939 (\lambda (d2: C).(\lambda (u2: T).(getl O c2 (CHead d2 (Bind Void) u2))))
940 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda (x3:
941 C).(\lambda (H16: (eq C x2 (CHead x3 (Bind Abbr) u1))).(\lambda (H17: (csuba
942 g x3 d1)).(let H18 \def (eq_ind C x2 (\lambda (c: C).(clear c2 c)) H13 (CHead
943 x3 (Bind Abbr) u1) H16) in (or3_intro0 (ex2 C (\lambda (d2: C).(getl O c2
944 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A
945 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl O c2 (CHead d2 (Bind
946 Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2
947 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
948 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
949 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl O c2 (CHead d2
950 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))
951 (ex_intro2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abbr) u1))) (\lambda
952 (d2: C).(csuba g d2 d1)) x3 (getl_intro O c2 (CHead x3 (Bind Abbr) u1) c2
953 (drop_refl c2) H18) H17)))))) H15)) (\lambda (H15: (ex4_3 C T A (\lambda (d2:
954 C).(\lambda (u2: T).(\lambda (_: A).(eq C x2 (CHead d2 (Bind Abst) u2)))))
955 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
956 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
957 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
958 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
959 A).(eq C x2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
960 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
961 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
962 (_: T).(\lambda (a: A).(arity g d1 u1 a)))) (or3 (ex2 C (\lambda (d2:
963 C).(getl O c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))
964 (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl O c2
965 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
966 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
967 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
968 (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
969 T).(getl O c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
970 T).(csuba g d2 d1))))) (\lambda (x3: C).(\lambda (x4: T).(\lambda (x5:
971 A).(\lambda (H16: (eq C x2 (CHead x3 (Bind Abst) x4))).(\lambda (H17: (csuba
972 g x3 d1)).(\lambda (H18: (arity g x3 x4 (asucc g x5))).(\lambda (H19: (arity
973 g d1 u1 x5)).(let H20 \def (eq_ind C x2 (\lambda (c: C).(clear c2 c)) H13
974 (CHead x3 (Bind Abst) x4) H16) in (or3_intro1 (ex2 C (\lambda (d2: C).(getl O
975 c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T
976 A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl O c2 (CHead d2
977 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
978 d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
979 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
980 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl O c2 (CHead d2
981 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))
982 (ex4_3_intro C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl O
983 c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
984 (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
985 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
986 (a: A).(arity g d1 u1 a)))) x3 x4 x5 (getl_intro O c2 (CHead x3 (Bind Abst)
987 x4) c2 (drop_refl c2) H20) H17 H18 H19)))))))))) H15)) (\lambda (H15: (ex2_2
988 C T (\lambda (d2: C).(\lambda (u2: T).(eq C x2 (CHead d2 (Bind Void) u2))))
989 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))).(ex2_2_ind C T (\lambda
990 (d2: C).(\lambda (u2: T).(eq C x2 (CHead d2 (Bind Void) u2)))) (\lambda (d2:
991 C).(\lambda (_: T).(csuba g d2 d1))) (or3 (ex2 C (\lambda (d2: C).(getl O c2
992 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A
993 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl O c2 (CHead d2 (Bind
994 Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2
995 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
996 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
997 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl O c2 (CHead d2
998 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))))
999 (\lambda (x3: C).(\lambda (x4: T).(\lambda (H16: (eq C x2 (CHead x3 (Bind
1000 Void) x4))).(\lambda (H17: (csuba g x3 d1)).(let H18 \def (eq_ind C x2
1001 (\lambda (c: C).(clear c2 c)) H13 (CHead x3 (Bind Void) x4) H16) in
1002 (or3_intro2 (ex2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind Abbr) u1)))
1003 (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda
1004 (u2: T).(\lambda (_: A).(getl O c2 (CHead d2 (Bind Abst) u2))))) (\lambda
1005 (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2:
1006 C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda
1007 (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex2_2 C T
1008 (\lambda (d2: C).(\lambda (u2: T).(getl O c2 (CHead d2 (Bind Void) u2))))
1009 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))) (ex2_2_intro C T (\lambda
1010 (d2: C).(\lambda (u2: T).(getl O c2 (CHead d2 (Bind Void) u2)))) (\lambda
1011 (d2: C).(\lambda (_: T).(csuba g d2 d1))) x3 x4 (getl_intro O c2 (CHead x3
1012 (Bind Void) x4) c2 (drop_refl c2) H18) H17))))))) H15)) H14)))))) H11))))))))
1013 (\lambda (n: nat).(\lambda (H8: ((\forall (x1: C).((drop n O x1 (CHead x0
1014 (Flat f) t)) \to (\forall (c2: C).((csuba g c2 x1) \to (or3 (ex2 C (\lambda
1015 (d2: C).(getl n c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
1016 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl n
1017 c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
1018 (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1019 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1020 (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
1021 T).(getl n c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
1022 T).(csuba g d2 d1))))))))))).(\lambda (x1: C).(\lambda (H9: (drop (S n) O x1
1023 (CHead x0 (Flat f) t))).(\lambda (c2: C).(\lambda (H10: (csuba g c2 x1)).(let
1024 H11 \def (drop_clear x1 (CHead x0 (Flat f) t) n H9) in (ex2_3_ind B C T
1025 (\lambda (b: B).(\lambda (e: C).(\lambda (v: T).(clear x1 (CHead e (Bind b)
1026 v))))) (\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop n O e (CHead x0
1027 (Flat f) t))))) (or3 (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind
1028 Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
1029 C).(\lambda (u2: T).(\lambda (_: A).(getl (S n) c2 (CHead d2 (Bind Abst)
1030 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
1031 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
1032 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
1033 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl (S n) c2 (CHead d2 (Bind
1034 Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda
1035 (x2: B).(\lambda (x3: C).(\lambda (x4: T).(\lambda (H12: (clear x1 (CHead x3
1036 (Bind x2) x4))).(\lambda (H13: (drop n O x3 (CHead x0 (Flat f) t))).(let H14
1037 \def (csuba_clear_trans g x1 c2 H10 (CHead x3 (Bind x2) x4) H12) in (ex2_ind
1038 C (\lambda (e2: C).(csuba g e2 (CHead x3 (Bind x2) x4))) (\lambda (e2:
1039 C).(clear c2 e2)) (or3 (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind
1040 Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
1041 C).(\lambda (u2: T).(\lambda (_: A).(getl (S n) c2 (CHead d2 (Bind Abst)
1042 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
1043 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
1044 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
1045 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl (S n) c2 (CHead d2 (Bind
1046 Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda
1047 (x5: C).(\lambda (H15: (csuba g x5 (CHead x3 (Bind x2) x4))).(\lambda (H16:
1048 (clear c2 x5)).(let H_x \def (csuba_gen_bind_rev g x2 x3 x5 x4 H15) in (let
1049 H17 \def H_x in (ex2_3_ind B C T (\lambda (b2: B).(\lambda (e2: C).(\lambda
1050 (v2: T).(eq C x5 (CHead e2 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2:
1051 C).(\lambda (_: T).(csuba g e2 x3)))) (or3 (ex2 C (\lambda (d2: C).(getl (S
1052 n) c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C
1053 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl (S n) c2 (CHead
1054 d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
1055 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1056 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1057 (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
1058 T).(getl (S n) c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
1059 T).(csuba g d2 d1))))) (\lambda (x6: B).(\lambda (x7: C).(\lambda (x8:
1060 T).(\lambda (H18: (eq C x5 (CHead x7 (Bind x6) x8))).(\lambda (H19: (csuba g
1061 x7 x3)).(let H20 \def (eq_ind C x5 (\lambda (c: C).(clear c2 c)) H16 (CHead
1062 x7 (Bind x6) x8) H18) in (let H21 \def (H8 x3 H13 x7 H19) in (or3_ind (ex2 C
1063 (\lambda (d2: C).(getl n x7 (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
1064 C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
1065 (_: A).(getl n x7 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
1066 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1067 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1068 (_: T).(\lambda (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2:
1069 C).(\lambda (u2: T).(getl n x7 (CHead d2 (Bind Void) u2)))) (\lambda (d2:
1070 C).(\lambda (_: T).(csuba g d2 d1)))) (or3 (ex2 C (\lambda (d2: C).(getl (S
1071 n) c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C
1072 T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl (S n) c2 (CHead
1073 d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
1074 A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1075 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1076 (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
1077 T).(getl (S n) c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
1078 T).(csuba g d2 d1))))) (\lambda (H22: (ex2 C (\lambda (d2: C).(getl n x7
1079 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1)))).(ex2_ind C
1080 (\lambda (d2: C).(getl n x7 (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
1081 C).(csuba g d2 d1)) (or3 (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2
1082 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
1083 (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl (S n) c2 (CHead d2 (Bind Abst)
1084 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
1085 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
1086 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
1087 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl (S n) c2 (CHead d2 (Bind
1088 Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))) (\lambda
1089 (x9: C).(\lambda (H23: (getl n x7 (CHead x9 (Bind Abbr) u1))).(\lambda (H24:
1090 (csuba g x9 d1)).(or3_intro0 (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2
1091 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda
1092 (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl (S n) c2 (CHead d2 (Bind Abst)
1093 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
1094 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
1095 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
1096 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl (S n) c2 (CHead d2 (Bind
1097 Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))) (ex_intro2 C
1098 (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2:
1099 C).(csuba g d2 d1)) x9 (getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind Abbr)
1100 u1) n H23) H24))))) H22)) (\lambda (H22: (ex4_3 C T A (\lambda (d2:
1101 C).(\lambda (u2: T).(\lambda (_: A).(getl n x7 (CHead d2 (Bind Abst) u2)))))
1102 (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda
1103 (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g a)))))
1104 (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1
1105 a)))))).(ex4_3_ind C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_:
1106 A).(getl n x7 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_:
1107 T).(\lambda (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2:
1108 T).(\lambda (a: A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda
1109 (_: T).(\lambda (a: A).(arity g d1 u1 a)))) (or3 (ex2 C (\lambda (d2:
1110 C).(getl (S n) c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
1111 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl (S
1112 n) c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
1113 (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1114 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1115 (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
1116 T).(getl (S n) c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
1117 T).(csuba g d2 d1))))) (\lambda (x9: C).(\lambda (x10: T).(\lambda (x11:
1118 A).(\lambda (H23: (getl n x7 (CHead x9 (Bind Abst) x10))).(\lambda (H24:
1119 (csuba g x9 d1)).(\lambda (H25: (arity g x9 x10 (asucc g x11))).(\lambda
1120 (H26: (arity g d1 u1 x11)).(or3_intro1 (ex2 C (\lambda (d2: C).(getl (S n) c2
1121 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A
1122 (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl (S n) c2 (CHead d2
1123 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g
1124 d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
1125 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1
1126 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl (S n) c2 (CHead
1127 d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))
1128 (ex4_3_intro C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl (S
1129 n) c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
1130 (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1131 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1132 (a: A).(arity g d1 u1 a)))) x9 x10 x11 (getl_clear_bind x6 c2 x7 x8 H20
1133 (CHead x9 (Bind Abst) x10) n H23) H24 H25 H26))))))))) H22)) (\lambda (H22:
1134 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl n x7 (CHead d2 (Bind Void)
1135 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))))).(ex2_2_ind C T
1136 (\lambda (d2: C).(\lambda (u2: T).(getl n x7 (CHead d2 (Bind Void) u2))))
1137 (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))) (or3 (ex2 C (\lambda (d2:
1138 C).(getl (S n) c2 (CHead d2 (Bind Abbr) u1))) (\lambda (d2: C).(csuba g d2
1139 d1))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl (S
1140 n) c2 (CHead d2 (Bind Abst) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda
1141 (_: A).(csuba g d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
1142 A).(arity g d2 u2 (asucc g a))))) (\lambda (_: C).(\lambda (_: T).(\lambda
1143 (a: A).(arity g d1 u1 a))))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
1144 T).(getl (S n) c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
1145 T).(csuba g d2 d1))))) (\lambda (x9: C).(\lambda (x10: T).(\lambda (H23:
1146 (getl n x7 (CHead x9 (Bind Void) x10))).(\lambda (H24: (csuba g x9
1147 d1)).(or3_intro2 (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind Abbr)
1148 u1))) (\lambda (d2: C).(csuba g d2 d1))) (ex4_3 C T A (\lambda (d2:
1149 C).(\lambda (u2: T).(\lambda (_: A).(getl (S n) c2 (CHead d2 (Bind Abst)
1150 u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d2 d1))))
1151 (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 (asucc g
1152 a))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 a)))))
1153 (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl (S n) c2 (CHead d2 (Bind
1154 Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))) (ex2_2_intro
1155 C T (\lambda (d2: C).(\lambda (u2: T).(getl (S n) c2 (CHead d2 (Bind Void)
1156 u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))) x9 x10
1157 (getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind Void) x10) n H23) H24))))))
1158 H22)) H21)))))))) H17)))))) H14))))))) H11)))))))) i) H7))))) k H3 H4)))))))
1159 x H1 H2)))) H0))))))).
projects / helm.git / blob