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/csubt/fwd.ma".
19 include "basic_1A/drop/fwd.ma".
21 lemma csubt_drop_flat:
22 \forall (g: G).(\forall (f: F).(\forall (n: nat).(\forall (c1: C).(\forall
23 (c2: C).((csubt g c1 c2) \to (\forall (d1: C).(\forall (u: T).((drop n O c1
24 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
25 (d2: C).(drop n O c2 (CHead d2 (Flat f) u))))))))))))
27 \lambda (g: G).(\lambda (f: F).(\lambda (n: nat).(nat_ind (\lambda (n0:
28 nat).(\forall (c1: C).(\forall (c2: C).((csubt g c1 c2) \to (\forall (d1:
29 C).(\forall (u: T).((drop n0 O c1 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda
30 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2 (CHead d2 (Flat f)
31 u))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubt g c1
32 c2)).(\lambda (d1: C).(\lambda (u: T).(\lambda (H0: (drop O O c1 (CHead d1
33 (Flat f) u))).(let H1 \def (eq_ind C c1 (\lambda (c: C).(csubt g c c2)) H
34 (CHead d1 (Flat f) u) (drop_gen_refl c1 (CHead d1 (Flat f) u) H0)) in (let
35 H_x \def (csubt_gen_flat g d1 c2 u f H1) in (let H2 \def H_x in (ex2_ind C
36 (\lambda (e2: C).(eq C c2 (CHead e2 (Flat f) u))) (\lambda (e2: C).(csubt g
37 d1 e2)) (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O
38 c2 (CHead d2 (Flat f) u)))) (\lambda (x: C).(\lambda (H3: (eq C c2 (CHead x
39 (Flat f) u))).(\lambda (H4: (csubt g d1 x)).(eq_ind_r C (CHead x (Flat f) u)
40 (\lambda (c: C).(ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
41 C).(drop O O c (CHead d2 (Flat f) u))))) (ex_intro2 C (\lambda (d2: C).(csubt
42 g d1 d2)) (\lambda (d2: C).(drop O O (CHead x (Flat f) u) (CHead d2 (Flat f)
43 u))) x H4 (drop_refl (CHead x (Flat f) u))) c2 H3)))) H2)))))))))) (\lambda
44 (n0: nat).(\lambda (H: ((\forall (c1: C).(\forall (c2: C).((csubt g c1 c2)
45 \to (\forall (d1: C).(\forall (u: T).((drop n0 O c1 (CHead d1 (Flat f) u))
46 \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2
47 (CHead d2 (Flat f) u)))))))))))).(\lambda (c1: C).(\lambda (c2: C).(\lambda
48 (H0: (csubt g c1 c2)).(csubt_ind g (\lambda (c: C).(\lambda (c0: C).(\forall
49 (d1: C).(\forall (u: T).((drop (S n0) O c (CHead d1 (Flat f) u)) \to (ex2 C
50 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c0 (CHead
51 d2 (Flat f) u))))))))) (\lambda (n1: nat).(\lambda (d1: C).(\lambda (u:
52 T).(\lambda (H1: (drop (S n0) O (CSort n1) (CHead d1 (Flat f) u))).(and3_ind
53 (eq C (CHead d1 (Flat f) u) (CSort n1)) (eq nat (S n0) O) (eq nat O O) (ex2 C
54 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1)
55 (CHead d2 (Flat f) u)))) (\lambda (_: (eq C (CHead d1 (Flat f) u) (CSort
56 n1))).(\lambda (H3: (eq nat (S n0) O)).(\lambda (_: (eq nat O O)).(let H5
57 \def (eq_ind nat (S n0) (\lambda (ee: nat).(match ee with [O \Rightarrow
58 False | (S _) \Rightarrow True])) I O H3) in (False_ind (ex2 C (\lambda (d2:
59 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2
60 (Flat f) u)))) H5))))) (drop_gen_sort n1 (S n0) O (CHead d1 (Flat f) u)
61 H1)))))) (\lambda (c0: C).(\lambda (c3: C).(\lambda (H1: (csubt g c0
62 c3)).(\lambda (H2: ((\forall (d1: C).(\forall (u: T).((drop (S n0) O c0
63 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
64 (d2: C).(drop (S n0) O c3 (CHead d2 (Flat f) u))))))))).(\lambda (k:
65 K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (d1: C).(\forall (u0:
66 T).((drop (S n0) O (CHead c0 k0 u) (CHead d1 (Flat f) u0)) \to (ex2 C
67 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
68 k0 u) (CHead d2 (Flat f) u0))))))))) (\lambda (b: B).(\lambda (u: T).(\lambda
69 (d1: C).(\lambda (u0: T).(\lambda (H3: (drop (S n0) O (CHead c0 (Bind b) u)
70 (CHead d1 (Flat f) u0))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2))
71 (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Flat f) u0))) (ex2 C (\lambda (d2:
72 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u)
73 (CHead d2 (Flat f) u0)))) (\lambda (x: C).(\lambda (H4: (csubt g d1
74 x)).(\lambda (H5: (drop n0 O c3 (CHead x (Flat f) u0))).(ex_intro2 C (\lambda
75 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b)
76 u) (CHead d2 (Flat f) u0))) x H4 (drop_drop (Bind b) n0 c3 (CHead x (Flat f)
77 u0) H5 u))))) (H c0 c3 H1 d1 u0 (drop_gen_drop (Bind b) c0 (CHead d1 (Flat f)
78 u0) u n0 H3)))))))) (\lambda (f0: F).(\lambda (u: T).(\lambda (d1:
79 C).(\lambda (u0: T).(\lambda (H3: (drop (S n0) O (CHead c0 (Flat f0) u)
80 (CHead d1 (Flat f) u0))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2))
81 (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Flat f) u0))) (ex2 C (\lambda
82 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f0)
83 u) (CHead d2 (Flat f) u0)))) (\lambda (x: C).(\lambda (H4: (csubt g d1
84 x)).(\lambda (H5: (drop (S n0) O c3 (CHead x (Flat f) u0))).(ex_intro2 C
85 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
86 (Flat f0) u) (CHead d2 (Flat f) u0))) x H4 (drop_drop (Flat f0) n0 c3 (CHead
87 x (Flat f) u0) H5 u))))) (H2 d1 u0 (drop_gen_drop (Flat f0) c0 (CHead d1
88 (Flat f) u0) u n0 H3)))))))) k)))))) (\lambda (c0: C).(\lambda (c3:
89 C).(\lambda (H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (u:
90 T).((drop (S n0) O c0 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda (d2:
91 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Flat f)
92 u))))))))).(\lambda (b: B).(\lambda (_: (not (eq B b Void))).(\lambda (u1:
93 T).(\lambda (u2: T).(\lambda (d1: C).(\lambda (u: T).(\lambda (H4: (drop (S
94 n0) O (CHead c0 (Bind Void) u1) (CHead d1 (Flat f) u))).(ex2_ind C (\lambda
95 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Flat f)
96 u))) (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
97 (CHead c3 (Bind b) u2) (CHead d2 (Flat f) u)))) (\lambda (x: C).(\lambda (H5:
98 (csubt g d1 x)).(\lambda (H6: (drop n0 O c3 (CHead x (Flat f) u))).(ex_intro2
99 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
100 (Bind b) u2) (CHead d2 (Flat f) u))) x H5 (drop_drop (Bind b) n0 c3 (CHead x
101 (Flat f) u) H6 u2))))) (H c0 c3 H1 d1 u (drop_gen_drop (Bind Void) c0 (CHead
102 d1 (Flat f) u) u1 n0 H4)))))))))))))) (\lambda (c0: C).(\lambda (c3:
103 C).(\lambda (H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (u:
104 T).((drop (S n0) O c0 (CHead d1 (Flat f) u)) \to (ex2 C (\lambda (d2:
105 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Flat f)
106 u))))))))).(\lambda (u: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 u
107 t)).(\lambda (_: (ty3 g c3 u t)).(\lambda (d1: C).(\lambda (u0: T).(\lambda
108 (H5: (drop (S n0) O (CHead c0 (Bind Abst) t) (CHead d1 (Flat f)
109 u0))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0
110 O c3 (CHead d2 (Flat f) u0))) (ex2 C (\lambda (d2: C).(csubt g d1 d2))
111 (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Flat f)
112 u0)))) (\lambda (x: C).(\lambda (H6: (csubt g d1 x)).(\lambda (H7: (drop n0 O
113 c3 (CHead x (Flat f) u0))).(ex_intro2 C (\lambda (d2: C).(csubt g d1 d2))
114 (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Flat f)
115 u0))) x H6 (drop_drop (Bind Abbr) n0 c3 (CHead x (Flat f) u0) H7 u))))) (H c0
116 c3 H1 d1 u0 (drop_gen_drop (Bind Abst) c0 (CHead d1 (Flat f) u0) t n0
117 H5)))))))))))))) c1 c2 H0)))))) n))).
119 lemma csubt_drop_abbr:
120 \forall (g: G).(\forall (n: nat).(\forall (c1: C).(\forall (c2: C).((csubt g
121 c1 c2) \to (\forall (d1: C).(\forall (u: T).((drop n O c1 (CHead d1 (Bind
122 Abbr) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
123 n O c2 (CHead d2 (Bind Abbr) u)))))))))))
125 \lambda (g: G).(\lambda (n: nat).(nat_ind (\lambda (n0: nat).(\forall (c1:
126 C).(\forall (c2: C).((csubt g c1 c2) \to (\forall (d1: C).(\forall (u:
127 T).((drop n0 O c1 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2:
128 C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2 (CHead d2 (Bind Abbr)
129 u))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubt g c1
130 c2)).(\lambda (d1: C).(\lambda (u: T).(\lambda (H0: (drop O O c1 (CHead d1
131 (Bind Abbr) u))).(let H1 \def (eq_ind C c1 (\lambda (c: C).(csubt g c c2)) H
132 (CHead d1 (Bind Abbr) u) (drop_gen_refl c1 (CHead d1 (Bind Abbr) u) H0)) in
133 (let H2 \def (csubt_gen_abbr g d1 c2 u H1) in (ex2_ind C (\lambda (e2: C).(eq
134 C c2 (CHead e2 (Bind Abbr) u))) (\lambda (e2: C).(csubt g d1 e2)) (ex2 C
135 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2
136 (Bind Abbr) u)))) (\lambda (x: C).(\lambda (H3: (eq C c2 (CHead x (Bind Abbr)
137 u))).(\lambda (H4: (csubt g d1 x)).(eq_ind_r C (CHead x (Bind Abbr) u)
138 (\lambda (c: C).(ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
139 C).(drop O O c (CHead d2 (Bind Abbr) u))))) (ex_intro2 C (\lambda (d2:
140 C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O (CHead x (Bind Abbr) u) (CHead
141 d2 (Bind Abbr) u))) x H4 (drop_refl (CHead x (Bind Abbr) u))) c2 H3))))
142 H2))))))))) (\lambda (n0: nat).(\lambda (H: ((\forall (c1: C).(\forall (c2:
143 C).((csubt g c1 c2) \to (\forall (d1: C).(\forall (u: T).((drop n0 O c1
144 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2))
145 (\lambda (d2: C).(drop n0 O c2 (CHead d2 (Bind Abbr) u)))))))))))).(\lambda
146 (c1: C).(\lambda (c2: C).(\lambda (H0: (csubt g c1 c2)).(csubt_ind g (\lambda
147 (c: C).(\lambda (c0: C).(\forall (d1: C).(\forall (u: T).((drop (S n0) O c
148 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2))
149 (\lambda (d2: C).(drop (S n0) O c0 (CHead d2 (Bind Abbr) u))))))))) (\lambda
150 (n1: nat).(\lambda (d1: C).(\lambda (u: T).(\lambda (H1: (drop (S n0) O
151 (CSort n1) (CHead d1 (Bind Abbr) u))).(and3_ind (eq C (CHead d1 (Bind Abbr)
152 u) (CSort n1)) (eq nat (S n0) O) (eq nat O O) (ex2 C (\lambda (d2: C).(csubt
153 g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr)
154 u)))) (\lambda (_: (eq C (CHead d1 (Bind Abbr) u) (CSort n1))).(\lambda (H3:
155 (eq nat (S n0) O)).(\lambda (_: (eq nat O O)).(let H5 \def (eq_ind nat (S n0)
156 (\lambda (ee: nat).(match ee with [O \Rightarrow False | (S _) \Rightarrow
157 True])) I O H3) in (False_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2))
158 (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u))))
159 H5))))) (drop_gen_sort n1 (S n0) O (CHead d1 (Bind Abbr) u) H1)))))) (\lambda
160 (c0: C).(\lambda (c3: C).(\lambda (H1: (csubt g c0 c3)).(\lambda (H2:
161 ((\forall (d1: C).(\forall (u: T).((drop (S n0) O c0 (CHead d1 (Bind Abbr)
162 u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S
163 n0) O c3 (CHead d2 (Bind Abbr) u))))))))).(\lambda (k: K).(K_ind (\lambda
164 (k0: K).(\forall (u: T).(\forall (d1: C).(\forall (u0: T).((drop (S n0) O
165 (CHead c0 k0 u) (CHead d1 (Bind Abbr) u0)) \to (ex2 C (\lambda (d2: C).(csubt
166 g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 k0 u) (CHead d2 (Bind
167 Abbr) u0))))))))) (\lambda (b: B).(\lambda (u: T).(\lambda (d1: C).(\lambda
168 (u0: T).(\lambda (H3: (drop (S n0) O (CHead c0 (Bind b) u) (CHead d1 (Bind
169 Abbr) u0))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
170 C).(drop n0 O c3 (CHead d2 (Bind Abbr) u0))) (ex2 C (\lambda (d2: C).(csubt g
171 d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind
172 Abbr) u0)))) (\lambda (x: C).(\lambda (H4: (csubt g d1 x)).(\lambda (H5:
173 (drop n0 O c3 (CHead x (Bind Abbr) u0))).(ex_intro2 C (\lambda (d2: C).(csubt
174 g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2
175 (Bind Abbr) u0))) x H4 (drop_drop (Bind b) n0 c3 (CHead x (Bind Abbr) u0) H5
176 u))))) (H c0 c3 H1 d1 u0 (drop_gen_drop (Bind b) c0 (CHead d1 (Bind Abbr) u0)
177 u n0 H3)))))))) (\lambda (f: F).(\lambda (u: T).(\lambda (d1: C).(\lambda
178 (u0: T).(\lambda (H3: (drop (S n0) O (CHead c0 (Flat f) u) (CHead d1 (Bind
179 Abbr) u0))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
180 C).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u0))) (ex2 C (\lambda (d2:
181 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f) u)
182 (CHead d2 (Bind Abbr) u0)))) (\lambda (x: C).(\lambda (H4: (csubt g d1
183 x)).(\lambda (H5: (drop (S n0) O c3 (CHead x (Bind Abbr) u0))).(ex_intro2 C
184 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
185 (Flat f) u) (CHead d2 (Bind Abbr) u0))) x H4 (drop_drop (Flat f) n0 c3 (CHead
186 x (Bind Abbr) u0) H5 u))))) (H2 d1 u0 (drop_gen_drop (Flat f) c0 (CHead d1
187 (Bind Abbr) u0) u n0 H3)))))))) k)))))) (\lambda (c0: C).(\lambda (c3:
188 C).(\lambda (H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (u:
189 T).((drop (S n0) O c0 (CHead d1 (Bind Abbr) u)) \to (ex2 C (\lambda (d2:
190 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abbr)
191 u))))))))).(\lambda (b: B).(\lambda (_: (not (eq B b Void))).(\lambda (u1:
192 T).(\lambda (u2: T).(\lambda (d1: C).(\lambda (u: T).(\lambda (H4: (drop (S
193 n0) O (CHead c0 (Bind Void) u1) (CHead d1 (Bind Abbr) u))).(ex2_ind C
194 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2
195 (Bind Abbr) u))) (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
196 C).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda
197 (x: C).(\lambda (H5: (csubt g d1 x)).(\lambda (H6: (drop n0 O c3 (CHead x
198 (Bind Abbr) u))).(ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
199 C).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u))) x H5
200 (drop_drop (Bind b) n0 c3 (CHead x (Bind Abbr) u) H6 u2))))) (H c0 c3 H1 d1 u
201 (drop_gen_drop (Bind Void) c0 (CHead d1 (Bind Abbr) u) u1 n0 H4))))))))))))))
202 (\lambda (c0: C).(\lambda (c3: C).(\lambda (H1: (csubt g c0 c3)).(\lambda (_:
203 ((\forall (d1: C).(\forall (u: T).((drop (S n0) O c0 (CHead d1 (Bind Abbr)
204 u)) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S
205 n0) O c3 (CHead d2 (Bind Abbr) u))))))))).(\lambda (u: T).(\lambda (t:
206 T).(\lambda (_: (ty3 g c0 u t)).(\lambda (_: (ty3 g c3 u t)).(\lambda (d1:
207 C).(\lambda (u0: T).(\lambda (H5: (drop (S n0) O (CHead c0 (Bind Abst) t)
208 (CHead d1 (Bind Abbr) u0))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2))
209 (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abbr) u0))) (ex2 C (\lambda
210 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind
211 Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (x: C).(\lambda (H6: (csubt g
212 d1 x)).(\lambda (H7: (drop n0 O c3 (CHead x (Bind Abbr) u0))).(ex_intro2 C
213 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
214 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0))) x H6 (drop_drop (Bind Abbr) n0 c3
215 (CHead x (Bind Abbr) u0) H7 u))))) (H c0 c3 H1 d1 u0 (drop_gen_drop (Bind
216 Abst) c0 (CHead d1 (Bind Abbr) u0) t n0 H5)))))))))))))) c1 c2 H0)))))) n)).
218 lemma csubt_drop_abst:
219 \forall (g: G).(\forall (n: nat).(\forall (c1: C).(\forall (c2: C).((csubt g
220 c1 c2) \to (\forall (d1: C).(\forall (t: T).((drop n O c1 (CHead d1 (Bind
221 Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
222 C).(drop n O c2 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
223 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop n
224 O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u
225 t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))))))))))
227 \lambda (g: G).(\lambda (n: nat).(nat_ind (\lambda (n0: nat).(\forall (c1:
228 C).(\forall (c2: C).((csubt g c1 c2) \to (\forall (d1: C).(\forall (t:
229 T).((drop n0 O c1 (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2:
230 C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2 (CHead d2 (Bind Abst)
231 t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
232 (d2: C).(\lambda (u: T).(drop n0 O c2 (CHead d2 (Bind Abbr) u)))) (\lambda
233 (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3
234 g d2 u t)))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubt g
235 c1 c2)).(\lambda (d1: C).(\lambda (t: T).(\lambda (H0: (drop O O c1 (CHead d1
236 (Bind Abst) t))).(let H1 \def (eq_ind C c1 (\lambda (c: C).(csubt g c c2)) H
237 (CHead d1 (Bind Abst) t) (drop_gen_refl c1 (CHead d1 (Bind Abst) t) H0)) in
238 (let H2 \def (csubt_gen_abst g d1 c2 t H1) in (or_ind (ex2 C (\lambda (e2:
239 C).(eq C c2 (CHead e2 (Bind Abst) t))) (\lambda (e2: C).(csubt g d1 e2)))
240 (ex4_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2 (Bind Abbr)
241 v2)))) (\lambda (e2: C).(\lambda (_: T).(csubt g d1 e2))) (\lambda (_:
242 C).(\lambda (v2: T).(ty3 g d1 v2 t))) (\lambda (e2: C).(\lambda (v2: T).(ty3
243 g e2 v2 t)))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
244 C).(drop O O c2 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
245 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O
246 O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u
247 t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))) (\lambda (H3: (ex2 C
248 (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abst) t))) (\lambda (e2: C).(csubt
249 g d1 e2)))).(ex2_ind C (\lambda (e2: C).(eq C c2 (CHead e2 (Bind Abst) t)))
250 (\lambda (e2: C).(csubt g d1 e2)) (or (ex2 C (\lambda (d2: C).(csubt g d1
251 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abst) t)))) (ex4_2 C T
252 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
253 (u: T).(drop O O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u:
254 T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))
255 (\lambda (x: C).(\lambda (H4: (eq C c2 (CHead x (Bind Abst) t))).(\lambda
256 (H5: (csubt g d1 x)).(eq_ind_r C (CHead x (Bind Abst) t) (\lambda (c: C).(or
257 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c (CHead
258 d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
259 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O c (CHead d2 (Bind Abbr)
260 u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2:
261 C).(\lambda (u: T).(ty3 g d2 u t)))))) (or_introl (ex2 C (\lambda (d2:
262 C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O (CHead x (Bind Abst) t) (CHead
263 d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
264 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O (CHead x (Bind Abst) t)
265 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t)))
266 (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))) (ex_intro2 C (\lambda (d2:
267 C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O (CHead x (Bind Abst) t) (CHead
268 d2 (Bind Abst) t))) x H5 (drop_refl (CHead x (Bind Abst) t)))) c2 H4)))) H3))
269 (\lambda (H3: (ex4_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2
270 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csubt g d1 e2)))
271 (\lambda (_: C).(\lambda (v2: T).(ty3 g d1 v2 t))) (\lambda (e2: C).(\lambda
272 (v2: T).(ty3 g e2 v2 t))))).(ex4_2_ind C T (\lambda (e2: C).(\lambda (v2:
273 T).(eq C c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_:
274 T).(csubt g d1 e2))) (\lambda (_: C).(\lambda (v2: T).(ty3 g d1 v2 t)))
275 (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 t))) (or (ex2 C (\lambda (d2:
276 C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abst) t))))
277 (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
278 C).(\lambda (u: T).(drop O O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_:
279 C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g
280 d2 u t))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H4: (eq C c2 (CHead
281 x0 (Bind Abbr) x1))).(\lambda (H5: (csubt g d1 x0)).(\lambda (H6: (ty3 g d1
282 x1 t)).(\lambda (H7: (ty3 g x0 x1 t)).(eq_ind_r C (CHead x0 (Bind Abbr) x1)
283 (\lambda (c: C).(or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
284 C).(drop O O c (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
285 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O
286 O c (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u
287 t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))) (or_intror (ex2 C
288 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O (CHead x0 (Bind
289 Abbr) x1) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda
290 (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O (CHead x0
291 (Bind Abbr) x1) (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u:
292 T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))
293 (ex4_2_intro C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
294 (d2: C).(\lambda (u: T).(drop O O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind
295 Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2:
296 C).(\lambda (u: T).(ty3 g d2 u t))) x0 x1 H5 (drop_refl (CHead x0 (Bind Abbr)
297 x1)) H6 H7)) c2 H4))))))) H3)) H2))))))))) (\lambda (n0: nat).(\lambda (H:
298 ((\forall (c1: C).(\forall (c2: C).((csubt g c1 c2) \to (\forall (d1:
299 C).(\forall (t: T).((drop n0 O c1 (CHead d1 (Bind Abst) t)) \to (or (ex2 C
300 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2 (CHead d2
301 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
302 d2))) (\lambda (d2: C).(\lambda (u: T).(drop n0 O c2 (CHead d2 (Bind Abbr)
303 u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2:
304 C).(\lambda (u: T).(ty3 g d2 u t))))))))))))).(\lambda (c1: C).(\lambda (c2:
305 C).(\lambda (H0: (csubt g c1 c2)).(csubt_ind g (\lambda (c: C).(\lambda (c0:
306 C).(\forall (d1: C).(\forall (t: T).((drop (S n0) O c (CHead d1 (Bind Abst)
307 t)) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
308 (S n0) O c0 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda
309 (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O c0
310 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t)))
311 (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))))))) (\lambda (n1:
312 nat).(\lambda (d1: C).(\lambda (t: T).(\lambda (H1: (drop (S n0) O (CSort n1)
313 (CHead d1 (Bind Abst) t))).(and3_ind (eq C (CHead d1 (Bind Abst) t) (CSort
314 n1)) (eq nat (S n0) O) (eq nat O O) (or (ex2 C (\lambda (d2: C).(csubt g d1
315 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abst) t))))
316 (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
317 C).(\lambda (u: T).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u))))
318 (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda
319 (u: T).(ty3 g d2 u t))))) (\lambda (_: (eq C (CHead d1 (Bind Abst) t) (CSort
320 n1))).(\lambda (H3: (eq nat (S n0) O)).(\lambda (_: (eq nat O O)).(let H5
321 \def (eq_ind nat (S n0) (\lambda (ee: nat).(match ee with [O \Rightarrow
322 False | (S _) \Rightarrow True])) I O H3) in (False_ind (or (ex2 C (\lambda
323 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2
324 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
325 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CSort n1) (CHead d2
326 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda
327 (d2: C).(\lambda (u: T).(ty3 g d2 u t))))) H5))))) (drop_gen_sort n1 (S n0) O
328 (CHead d1 (Bind Abst) t) H1)))))) (\lambda (c0: C).(\lambda (c3: C).(\lambda
329 (H1: (csubt g c0 c3)).(\lambda (H2: ((\forall (d1: C).(\forall (t: T).((drop
330 (S n0) O c0 (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt
331 g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst) t))))
332 (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
333 C).(\lambda (u: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u)))) (\lambda (_:
334 C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g
335 d2 u t)))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u:
336 T).(\forall (d1: C).(\forall (t: T).((drop (S n0) O (CHead c0 k0 u) (CHead d1
337 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
338 (d2: C).(drop (S n0) O (CHead c3 k0 u) (CHead d2 (Bind Abst) t)))) (ex4_2 C T
339 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
340 (u0: T).(drop (S n0) O (CHead c3 k0 u) (CHead d2 (Bind Abbr) u0)))) (\lambda
341 (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0:
342 T).(ty3 g d2 u0 t)))))))))) (\lambda (b: B).(\lambda (u: T).(\lambda (d1:
343 C).(\lambda (t: T).(\lambda (H3: (drop (S n0) O (CHead c0 (Bind b) u) (CHead
344 d1 (Bind Abst) t))).(or_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
345 (d2: C).(drop n0 O c3 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
346 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
347 n0 O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g
348 d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t)))) (or (ex2 C
349 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
350 (Bind b) u) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda
351 (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O
352 (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda
353 (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0
354 t))))) (\lambda (H4: (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
355 C).(drop n0 O c3 (CHead d2 (Bind Abst) t))))).(ex2_ind C (\lambda (d2:
356 C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abst) t)))
357 (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
358 (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
359 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
360 (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (_:
361 C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3
362 g d2 u0 t))))) (\lambda (x: C).(\lambda (H5: (csubt g d1 x)).(\lambda (H6:
363 (drop n0 O c3 (CHead x (Bind Abst) t))).(or_introl (ex2 C (\lambda (d2:
364 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u)
365 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_:
366 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
367 c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0:
368 T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))))
369 (ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0)
370 O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t))) x H5 (drop_drop (Bind b)
371 n0 c3 (CHead x (Bind Abst) t) H6 u)))))) H4)) (\lambda (H4: (ex4_2 C T
372 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
373 (u0: T).(drop n0 O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda
374 (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0
375 t))))).(ex4_2_ind C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2)))
376 (\lambda (d2: C).(\lambda (u0: T).(drop n0 O c3 (CHead d2 (Bind Abbr) u0))))
377 (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda
378 (u0: T).(ty3 g d2 u0 t))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2))
379 (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst)
380 t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
381 (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind
382 Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2:
383 C).(\lambda (u0: T).(ty3 g d2 u0 t))))) (\lambda (x0: C).(\lambda (x1:
384 T).(\lambda (H5: (csubt g d1 x0)).(\lambda (H6: (drop n0 O c3 (CHead x0 (Bind
385 Abbr) x1))).(\lambda (H7: (ty3 g d1 x1 t)).(\lambda (H8: (ty3 g x0 x1
386 t)).(or_intror (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
387 C).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)))) (ex4_2 C
388 T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
389 C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind
390 Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2:
391 C).(\lambda (u0: T).(ty3 g d2 u0 t)))) (ex4_2_intro C T (\lambda (d2:
392 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
393 (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (_:
394 C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3
395 g d2 u0 t))) x0 x1 H5 (drop_drop (Bind b) n0 c3 (CHead x0 (Bind Abbr) x1) H6
396 u) H7 H8)))))))) H4)) (H c0 c3 H1 d1 t (drop_gen_drop (Bind b) c0 (CHead d1
397 (Bind Abst) t) u n0 H3)))))))) (\lambda (f: F).(\lambda (u: T).(\lambda (d1:
398 C).(\lambda (t: T).(\lambda (H3: (drop (S n0) O (CHead c0 (Flat f) u) (CHead
399 d1 (Bind Abst) t))).(or_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
400 (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda
401 (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0:
402 T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda
403 (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0
404 t)))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S
405 n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda
406 (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0:
407 T).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)))) (\lambda
408 (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0:
409 T).(ty3 g d2 u0 t))))) (\lambda (H4: (ex2 C (\lambda (d2: C).(csubt g d1 d2))
410 (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst) t))))).(ex2_ind C
411 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead
412 d2 (Bind Abst) t))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
413 (d2: C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t))))
414 (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
415 C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind
416 Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2:
417 C).(\lambda (u0: T).(ty3 g d2 u0 t))))) (\lambda (x: C).(\lambda (H5: (csubt
418 g d1 x)).(\lambda (H6: (drop (S n0) O c3 (CHead x (Bind Abst) t))).(or_introl
419 (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O
420 (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
421 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
422 (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (_:
423 C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3
424 g d2 u0 t)))) (ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
425 C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t))) x H5
426 (drop_drop (Flat f) n0 c3 (CHead x (Bind Abst) t) H6 u)))))) H4)) (\lambda
427 (H4: (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
428 (d2: C).(\lambda (u0: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u0))))
429 (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda
430 (u0: T).(ty3 g d2 u0 t))))).(ex4_2_ind C T (\lambda (d2: C).(\lambda (_:
431 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O c3
432 (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0
433 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))) (or (ex2 C (\lambda
434 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f)
435 u) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_:
436 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead
437 c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0:
438 T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t)))))
439 (\lambda (x0: C).(\lambda (x1: T).(\lambda (H5: (csubt g d1 x0)).(\lambda
440 (H6: (drop (S n0) O c3 (CHead x0 (Bind Abbr) x1))).(\lambda (H7: (ty3 g d1 x1
441 t)).(\lambda (H8: (ty3 g x0 x1 t)).(or_intror (ex2 C (\lambda (d2: C).(csubt
442 g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2
443 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
444 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Flat f) u)
445 (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0
446 t))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t)))) (ex4_2_intro C T
447 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
448 (u0: T).(drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0))))
449 (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda
450 (u0: T).(ty3 g d2 u0 t))) x0 x1 H5 (drop_drop (Flat f) n0 c3 (CHead x0 (Bind
451 Abbr) x1) H6 u) H7 H8)))))))) H4)) (H2 d1 t (drop_gen_drop (Flat f) c0 (CHead
452 d1 (Bind Abst) t) u n0 H3)))))))) k)))))) (\lambda (c0: C).(\lambda (c3:
453 C).(\lambda (H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (t:
454 T).((drop (S n0) O c0 (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2:
455 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst)
456 t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
457 (d2: C).(\lambda (u: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u))))
458 (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda
459 (u: T).(ty3 g d2 u t)))))))))).(\lambda (b: B).(\lambda (_: (not (eq B b
460 Void))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (d1: C).(\lambda (t:
461 T).(\lambda (H4: (drop (S n0) O (CHead c0 (Bind Void) u1) (CHead d1 (Bind
462 Abst) t))).(or_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
463 C).(drop n0 O c3 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
464 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop
465 n0 O c3 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1
466 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))) (or (ex2 C (\lambda
467 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b)
468 u2) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_:
469 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CHead
470 c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u:
471 T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))
472 (\lambda (H5: (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
473 n0 O c3 (CHead d2 (Bind Abst) t))))).(ex2_ind C (\lambda (d2: C).(csubt g d1
474 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abst) t))) (or (ex2 C
475 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
476 (Bind b) u2) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda
477 (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O
478 (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda
479 (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))
480 (\lambda (x: C).(\lambda (H6: (csubt g d1 x)).(\lambda (H7: (drop n0 O c3
481 (CHead x (Bind Abst) t))).(or_introl (ex2 C (\lambda (d2: C).(csubt g d1 d2))
482 (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst)
483 t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
484 (d2: C).(\lambda (u: T).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind
485 Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2:
486 C).(\lambda (u: T).(ty3 g d2 u t)))) (ex_intro2 C (\lambda (d2: C).(csubt g
487 d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2
488 (Bind Abst) t))) x H6 (drop_drop (Bind b) n0 c3 (CHead x (Bind Abst) t) H7
489 u2)))))) H5)) (\lambda (H5: (ex4_2 C T (\lambda (d2: C).(\lambda (_:
490 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop n0 O c3 (CHead d2
491 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda
492 (d2: C).(\lambda (u: T).(ty3 g d2 u t))))).(ex4_2_ind C T (\lambda (d2:
493 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop
494 n0 O c3 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1
495 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))) (or (ex2 C (\lambda
496 (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b)
497 u2) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_:
498 T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CHead
499 c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u:
500 T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))
501 (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (csubt g d1 x0)).(\lambda
502 (H7: (drop n0 O c3 (CHead x0 (Bind Abbr) x1))).(\lambda (H8: (ty3 g d1 x1
503 t)).(\lambda (H9: (ty3 g x0 x1 t)).(or_intror (ex2 C (\lambda (d2: C).(csubt
504 g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2
505 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
506 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CHead c3 (Bind b) u2)
507 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t)))
508 (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))) (ex4_2_intro C T (\lambda
509 (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u:
510 T).(drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)))) (\lambda
511 (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3
512 g d2 u t))) x0 x1 H6 (drop_drop (Bind b) n0 c3 (CHead x0 (Bind Abbr) x1) H7
513 u2) H8 H9)))))))) H5)) (H c0 c3 H1 d1 t (drop_gen_drop (Bind Void) c0 (CHead
514 d1 (Bind Abst) t) u1 n0 H4)))))))))))))) (\lambda (c0: C).(\lambda (c3:
515 C).(\lambda (H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (t:
516 T).((drop (S n0) O c0 (CHead d1 (Bind Abst) t)) \to (or (ex2 C (\lambda (d2:
517 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3 (CHead d2 (Bind Abst)
518 t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
519 (d2: C).(\lambda (u: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u))))
520 (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda
521 (u: T).(ty3 g d2 u t)))))))))).(\lambda (u: T).(\lambda (t: T).(\lambda (_:
522 (ty3 g c0 u t)).(\lambda (_: (ty3 g c3 u t)).(\lambda (d1: C).(\lambda (t0:
523 T).(\lambda (H5: (drop (S n0) O (CHead c0 (Bind Abst) t) (CHead d1 (Bind
524 Abst) t0))).(or_ind (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
525 C).(drop n0 O c3 (CHead d2 (Bind Abst) t0)))) (ex4_2 C T (\lambda (d2:
526 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
527 n0 O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g
528 d1 u0 t0))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t0)))) (or (ex2 C
529 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3
530 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)))) (ex4_2 C T (\lambda (d2:
531 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
532 (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (_:
533 C).(\lambda (u0: T).(ty3 g d1 u0 t0))) (\lambda (d2: C).(\lambda (u0: T).(ty3
534 g d2 u0 t0))))) (\lambda (H6: (ex2 C (\lambda (d2: C).(csubt g d1 d2))
535 (\lambda (d2: C).(drop n0 O c3 (CHead d2 (Bind Abst) t0))))).(ex2_ind C
536 (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3 (CHead d2
537 (Bind Abst) t0))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
538 C).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0))))
539 (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
540 C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind
541 Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t0))) (\lambda
542 (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t0))))) (\lambda (x: C).(\lambda (H7:
543 (csubt g d1 x)).(\lambda (H8: (drop n0 O c3 (CHead x (Bind Abst)
544 t0))).(or_introl (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
545 C).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0))))
546 (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
547 C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind
548 Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t0))) (\lambda
549 (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t0)))) (ex_intro2 C (\lambda (d2:
550 C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind Abbr) u)
551 (CHead d2 (Bind Abst) t0))) x H7 (drop_drop (Bind Abbr) n0 c3 (CHead x (Bind
552 Abst) t0) H8 u)))))) H6)) (\lambda (H6: (ex4_2 C T (\lambda (d2: C).(\lambda
553 (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop n0 O c3
554 (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0
555 t0))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t0))))).(ex4_2_ind C T
556 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
557 (u0: T).(drop n0 O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda (_: C).(\lambda
558 (u0: T).(ty3 g d1 u0 t0))) (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0
559 t0))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S
560 n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)))) (ex4_2 C T
561 (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
562 (u0: T).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0))))
563 (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t0))) (\lambda (d2: C).(\lambda
564 (u0: T).(ty3 g d2 u0 t0))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H7:
565 (csubt g d1 x0)).(\lambda (H8: (drop n0 O c3 (CHead x0 (Bind Abbr)
566 x1))).(\lambda (H9: (ty3 g d1 x1 t0)).(\lambda (H10: (ty3 g x0 x1
567 t0)).(or_intror (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
568 C).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0))))
569 (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
570 C).(\lambda (u0: T).(drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind
571 Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t0))) (\lambda
572 (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t0)))) (ex4_2_intro C T (\lambda (d2:
573 C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u0: T).(drop
574 (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)))) (\lambda (_:
575 C).(\lambda (u0: T).(ty3 g d1 u0 t0))) (\lambda (d2: C).(\lambda (u0: T).(ty3
576 g d2 u0 t0))) x0 x1 H7 (drop_drop (Bind Abbr) n0 c3 (CHead x0 (Bind Abbr) x1)
577 H8 u) H9 H10)))))))) H6)) (H c0 c3 H1 d1 t0 (drop_gen_drop (Bind Abst) c0
578 (CHead d1 (Bind Abst) t0) t n0 H5)))))))))))))) c1 c2 H0)))))) n)).