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