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