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