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