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