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