1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "Basic-1/wcpr0/defs.ma".
19 include "Basic-1/getl/props.ma".
22 \forall (c1: C).(\forall (c2: C).((wcpr0 c1 c2) \to (\forall (h:
23 nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((drop h O c1 (CHead
24 e1 k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(drop h O c2
25 (CHead e2 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda
26 (_: C).(\lambda (u2: T).(pr0 u1 u2)))))))))))
28 \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (wcpr0 c1 c2)).(wcpr0_ind
29 (\lambda (c: C).(\lambda (c0: C).(\forall (h: nat).(\forall (e1: C).(\forall
30 (u1: T).(\forall (k: K).((drop h O c (CHead e1 k u1)) \to (ex3_2 C T (\lambda
31 (e2: C).(\lambda (u2: T).(drop h O c0 (CHead e2 k u2)))) (\lambda (e2:
32 C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u2: T).(pr0 u1
33 u2))))))))))) (\lambda (c: C).(\lambda (h: nat).(\lambda (e1: C).(\lambda
34 (u1: T).(\lambda (k: K).(\lambda (H0: (drop h O c (CHead e1 k
35 u1))).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u2: T).(drop h O c (CHead
36 e2 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_:
37 C).(\lambda (u2: T).(pr0 u1 u2))) e1 u1 H0 (wcpr0_refl e1) (pr0_refl
38 u1)))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (wcpr0 c3
39 c4)).(\lambda (H1: ((\forall (h: nat).(\forall (e1: C).(\forall (u1:
40 T).(\forall (k: K).((drop h O c3 (CHead e1 k u1)) \to (ex3_2 C T (\lambda
41 (e2: C).(\lambda (u2: T).(drop h O c4 (CHead e2 k u2)))) (\lambda (e2:
42 C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u2: T).(pr0 u1
43 u2))))))))))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H2: (pr0 u1
44 u2)).(\lambda (k: K).(\lambda (h: nat).(nat_ind (\lambda (n: nat).(\forall
45 (e1: C).(\forall (u3: T).(\forall (k0: K).((drop n O (CHead c3 k u1) (CHead
46 e1 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead
47 c4 k u2) (CHead e2 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2)))
48 (\lambda (_: C).(\lambda (u4: T).(pr0 u3 u4))))))))) (\lambda (e1:
49 C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H3: (drop O O (CHead c3 k u1)
50 (CHead e1 k0 u0))).(let H4 \def (f_equal C C (\lambda (e: C).(match e in C
51 return (\lambda (_: C).C) with [(CSort _) \Rightarrow c3 | (CHead c _ _)
52 \Rightarrow c])) (CHead c3 k u1) (CHead e1 k0 u0) (drop_gen_refl (CHead c3 k
53 u1) (CHead e1 k0 u0) H3)) in ((let H5 \def (f_equal C K (\lambda (e:
54 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
55 (CHead _ k1 _) \Rightarrow k1])) (CHead c3 k u1) (CHead e1 k0 u0)
56 (drop_gen_refl (CHead c3 k u1) (CHead e1 k0 u0) H3)) in ((let H6 \def
57 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
58 [(CSort _) \Rightarrow u1 | (CHead _ _ t) \Rightarrow t])) (CHead c3 k u1)
59 (CHead e1 k0 u0) (drop_gen_refl (CHead c3 k u1) (CHead e1 k0 u0) H3)) in
60 (\lambda (H7: (eq K k k0)).(\lambda (H8: (eq C c3 e1)).(eq_ind K k (\lambda
61 (k1: K).(ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(drop O O (CHead c4 k
62 u2) (CHead e2 k1 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2)))
63 (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))))) (eq_ind T u1 (\lambda (t:
64 T).(ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(drop O O (CHead c4 k u2)
65 (CHead e2 k u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda
66 (_: C).(\lambda (u3: T).(pr0 t u3))))) (eq_ind C c3 (\lambda (c: C).(ex3_2 C
67 T (\lambda (e2: C).(\lambda (u3: T).(drop O O (CHead c4 k u2) (CHead e2 k
68 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 c e2))) (\lambda (_:
69 C).(\lambda (u3: T).(pr0 u1 u3))))) (ex3_2_intro C T (\lambda (e2:
70 C).(\lambda (u3: T).(drop O O (CHead c4 k u2) (CHead e2 k u3)))) (\lambda
71 (e2: C).(\lambda (_: T).(wcpr0 c3 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0
72 u1 u3))) c4 u2 (drop_refl (CHead c4 k u2)) H0 H2) e1 H8) u0 H6) k0 H7))))
73 H5)) H4)))))) (K_ind (\lambda (k0: K).(\forall (n: nat).(((\forall (e1:
74 C).(\forall (u3: T).(\forall (k1: K).((drop n O (CHead c3 k0 u1) (CHead e1 k1
75 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead c4 k0
76 u2) (CHead e2 k1 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2)))
77 (\lambda (_: C).(\lambda (u4: T).(pr0 u3 u4))))))))) \to (\forall (e1:
78 C).(\forall (u3: T).(\forall (k1: K).((drop (S n) O (CHead c3 k0 u1) (CHead
79 e1 k1 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(drop (S n) O
80 (CHead c4 k0 u2) (CHead e2 k1 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0
81 e1 e2))) (\lambda (_: C).(\lambda (u4: T).(pr0 u3 u4))))))))))) (\lambda (b:
82 B).(\lambda (n: nat).(\lambda (_: ((\forall (e1: C).(\forall (u3: T).(\forall
83 (k0: K).((drop n O (CHead c3 (Bind b) u1) (CHead e1 k0 u3)) \to (ex3_2 C T
84 (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead c4 (Bind b) u2) (CHead e2
85 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_:
86 C).(\lambda (u4: T).(pr0 u3 u4)))))))))).(\lambda (e1: C).(\lambda (u0:
87 T).(\lambda (k0: K).(\lambda (H4: (drop (S n) O (CHead c3 (Bind b) u1) (CHead
88 e1 k0 u0))).(let H5 \def (H1 n e1 u0 k0 (drop_gen_drop (Bind b) c3 (CHead e1
89 k0 u0) u1 n H4)) in (ex3_2_ind C T (\lambda (e2: C).(\lambda (u3: T).(drop n
90 O c4 (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2)))
91 (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))) (ex3_2 C T (\lambda (e2:
92 C).(\lambda (u3: T).(drop (S n) O (CHead c4 (Bind b) u2) (CHead e2 k0 u3))))
93 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda
94 (u3: T).(pr0 u0 u3)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (drop
95 n O c4 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 e1 x0)).(\lambda (H8: (pr0 u0
96 x1)).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u3: T).(drop (S n) O (CHead
97 c4 (Bind b) u2) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0
98 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))) x0 x1 (drop_drop
99 (Bind b) n c4 (CHead x0 k0 x1) H6 u2) H7 H8)))))) H5))))))))) (\lambda (f:
100 F).(\lambda (n: nat).(\lambda (_: ((\forall (e1: C).(\forall (u3: T).(\forall
101 (k0: K).((drop n O (CHead c3 (Flat f) u1) (CHead e1 k0 u3)) \to (ex3_2 C T
102 (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead c4 (Flat f) u2) (CHead e2
103 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_:
104 C).(\lambda (u4: T).(pr0 u3 u4)))))))))).(\lambda (e1: C).(\lambda (u0:
105 T).(\lambda (k0: K).(\lambda (H4: (drop (S n) O (CHead c3 (Flat f) u1) (CHead
106 e1 k0 u0))).(let H5 \def (H1 (S n) e1 u0 k0 (drop_gen_drop (Flat f) c3 (CHead
107 e1 k0 u0) u1 n H4)) in (ex3_2_ind C T (\lambda (e2: C).(\lambda (u3: T).(drop
108 (S n) O c4 (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1
109 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))) (ex3_2 C T (\lambda (e2:
110 C).(\lambda (u3: T).(drop (S n) O (CHead c4 (Flat f) u2) (CHead e2 k0 u3))))
111 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda
112 (u3: T).(pr0 u0 u3)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (drop
113 (S n) O c4 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 e1 x0)).(\lambda (H8: (pr0
114 u0 x1)).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u3: T).(drop (S n) O
115 (CHead c4 (Flat f) u2) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_:
116 T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))) x0 x1
117 (drop_drop (Flat f) n c4 (CHead x0 k0 x1) H6 u2) H7 H8)))))) H5))))))))) k)
118 h)))))))))) c1 c2 H))).
123 theorem wcpr0_drop_back:
124 \forall (c1: C).(\forall (c2: C).((wcpr0 c2 c1) \to (\forall (h:
125 nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((drop h O c1 (CHead
126 e1 k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(drop h O c2
127 (CHead e2 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda
128 (_: C).(\lambda (u2: T).(pr0 u2 u1)))))))))))
130 \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (wcpr0 c2 c1)).(wcpr0_ind
131 (\lambda (c: C).(\lambda (c0: C).(\forall (h: nat).(\forall (e1: C).(\forall
132 (u1: T).(\forall (k: K).((drop h O c0 (CHead e1 k u1)) \to (ex3_2 C T
133 (\lambda (e2: C).(\lambda (u2: T).(drop h O c (CHead e2 k u2)))) (\lambda
134 (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u2: T).(pr0
135 u2 u1))))))))))) (\lambda (c: C).(\lambda (h: nat).(\lambda (e1: C).(\lambda
136 (u1: T).(\lambda (k: K).(\lambda (H0: (drop h O c (CHead e1 k
137 u1))).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u2: T).(drop h O c (CHead
138 e2 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_:
139 C).(\lambda (u2: T).(pr0 u2 u1))) e1 u1 H0 (wcpr0_refl e1) (pr0_refl
140 u1)))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (wcpr0 c3
141 c4)).(\lambda (H1: ((\forall (h: nat).(\forall (e1: C).(\forall (u1:
142 T).(\forall (k: K).((drop h O c4 (CHead e1 k u1)) \to (ex3_2 C T (\lambda
143 (e2: C).(\lambda (u2: T).(drop h O c3 (CHead e2 k u2)))) (\lambda (e2:
144 C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u2: T).(pr0 u2
145 u1))))))))))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H2: (pr0 u1
146 u2)).(\lambda (k: K).(\lambda (h: nat).(nat_ind (\lambda (n: nat).(\forall
147 (e1: C).(\forall (u3: T).(\forall (k0: K).((drop n O (CHead c4 k u2) (CHead
148 e1 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead
149 c3 k u1) (CHead e2 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1)))
150 (\lambda (_: C).(\lambda (u4: T).(pr0 u4 u3))))))))) (\lambda (e1:
151 C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H3: (drop O O (CHead c4 k u2)
152 (CHead e1 k0 u0))).(let H4 \def (f_equal C C (\lambda (e: C).(match e in C
153 return (\lambda (_: C).C) with [(CSort _) \Rightarrow c4 | (CHead c _ _)
154 \Rightarrow c])) (CHead c4 k u2) (CHead e1 k0 u0) (drop_gen_refl (CHead c4 k
155 u2) (CHead e1 k0 u0) H3)) in ((let H5 \def (f_equal C K (\lambda (e:
156 C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
157 (CHead _ k1 _) \Rightarrow k1])) (CHead c4 k u2) (CHead e1 k0 u0)
158 (drop_gen_refl (CHead c4 k u2) (CHead e1 k0 u0) H3)) in ((let H6 \def
159 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
160 [(CSort _) \Rightarrow u2 | (CHead _ _ t) \Rightarrow t])) (CHead c4 k u2)
161 (CHead e1 k0 u0) (drop_gen_refl (CHead c4 k u2) (CHead e1 k0 u0) H3)) in
162 (\lambda (H7: (eq K k k0)).(\lambda (H8: (eq C c4 e1)).(eq_ind K k (\lambda
163 (k1: K).(ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(drop O O (CHead c3 k
164 u1) (CHead e2 k1 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1)))
165 (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))))) (eq_ind T u2 (\lambda (t:
166 T).(ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(drop O O (CHead c3 k u1)
167 (CHead e2 k u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda
168 (_: C).(\lambda (u3: T).(pr0 u3 t))))) (eq_ind C c4 (\lambda (c: C).(ex3_2 C
169 T (\lambda (e2: C).(\lambda (u3: T).(drop O O (CHead c3 k u1) (CHead e2 k
170 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 c))) (\lambda (_:
171 C).(\lambda (u3: T).(pr0 u3 u2))))) (ex3_2_intro C T (\lambda (e2:
172 C).(\lambda (u3: T).(drop O O (CHead c3 k u1) (CHead e2 k u3)))) (\lambda
173 (e2: C).(\lambda (_: T).(wcpr0 e2 c4))) (\lambda (_: C).(\lambda (u3: T).(pr0
174 u3 u2))) c3 u1 (drop_refl (CHead c3 k u1)) H0 H2) e1 H8) u0 H6) k0 H7))))
175 H5)) H4)))))) (K_ind (\lambda (k0: K).(\forall (n: nat).(((\forall (e1:
176 C).(\forall (u3: T).(\forall (k1: K).((drop n O (CHead c4 k0 u2) (CHead e1 k1
177 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead c3 k0
178 u1) (CHead e2 k1 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1)))
179 (\lambda (_: C).(\lambda (u4: T).(pr0 u4 u3))))))))) \to (\forall (e1:
180 C).(\forall (u3: T).(\forall (k1: K).((drop (S n) O (CHead c4 k0 u2) (CHead
181 e1 k1 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(drop (S n) O
182 (CHead c3 k0 u1) (CHead e2 k1 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0
183 e2 e1))) (\lambda (_: C).(\lambda (u4: T).(pr0 u4 u3))))))))))) (\lambda (b:
184 B).(\lambda (n: nat).(\lambda (_: ((\forall (e1: C).(\forall (u3: T).(\forall
185 (k0: K).((drop n O (CHead c4 (Bind b) u2) (CHead e1 k0 u3)) \to (ex3_2 C T
186 (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead c3 (Bind b) u1) (CHead e2
187 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_:
188 C).(\lambda (u4: T).(pr0 u4 u3)))))))))).(\lambda (e1: C).(\lambda (u0:
189 T).(\lambda (k0: K).(\lambda (H4: (drop (S n) O (CHead c4 (Bind b) u2) (CHead
190 e1 k0 u0))).(let H5 \def (H1 n e1 u0 k0 (drop_gen_drop (Bind b) c4 (CHead e1
191 k0 u0) u2 n H4)) in (ex3_2_ind C T (\lambda (e2: C).(\lambda (u3: T).(drop n
192 O c3 (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1)))
193 (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))) (ex3_2 C T (\lambda (e2:
194 C).(\lambda (u3: T).(drop (S n) O (CHead c3 (Bind b) u1) (CHead e2 k0 u3))))
195 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda
196 (u3: T).(pr0 u3 u0)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (drop
197 n O c3 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 x0 e1)).(\lambda (H8: (pr0 x1
198 u0)).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u3: T).(drop (S n) O (CHead
199 c3 (Bind b) u1) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0
200 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))) x0 x1 (drop_drop
201 (Bind b) n c3 (CHead x0 k0 x1) H6 u1) H7 H8)))))) H5))))))))) (\lambda (f:
202 F).(\lambda (n: nat).(\lambda (_: ((\forall (e1: C).(\forall (u3: T).(\forall
203 (k0: K).((drop n O (CHead c4 (Flat f) u2) (CHead e1 k0 u3)) \to (ex3_2 C T
204 (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead c3 (Flat f) u1) (CHead e2
205 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_:
206 C).(\lambda (u4: T).(pr0 u4 u3)))))))))).(\lambda (e1: C).(\lambda (u0:
207 T).(\lambda (k0: K).(\lambda (H4: (drop (S n) O (CHead c4 (Flat f) u2) (CHead
208 e1 k0 u0))).(let H5 \def (H1 (S n) e1 u0 k0 (drop_gen_drop (Flat f) c4 (CHead
209 e1 k0 u0) u2 n H4)) in (ex3_2_ind C T (\lambda (e2: C).(\lambda (u3: T).(drop
210 (S n) O c3 (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2
211 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))) (ex3_2 C T (\lambda (e2:
212 C).(\lambda (u3: T).(drop (S n) O (CHead c3 (Flat f) u1) (CHead e2 k0 u3))))
213 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda
214 (u3: T).(pr0 u3 u0)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (drop
215 (S n) O c3 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 x0 e1)).(\lambda (H8: (pr0
216 x1 u0)).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u3: T).(drop (S n) O
217 (CHead c3 (Flat f) u1) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_:
218 T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))) x0 x1
219 (drop_drop (Flat f) n c3 (CHead x0 k0 x1) H6 u1) H7 H8)))))) H5))))))))) k)
220 h)))))))))) c2 c1 H))).
226 \forall (c1: C).(\forall (c2: C).((wcpr0 c1 c2) \to (\forall (h:
227 nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((getl h c1 (CHead e1
228 k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(getl h c2 (CHead e2
229 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_:
230 C).(\lambda (u2: T).(pr0 u1 u2)))))))))))
232 \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (wcpr0 c1 c2)).(wcpr0_ind
233 (\lambda (c: C).(\lambda (c0: C).(\forall (h: nat).(\forall (e1: C).(\forall
234 (u1: T).(\forall (k: K).((getl h c (CHead e1 k u1)) \to (ex3_2 C T (\lambda
235 (e2: C).(\lambda (u2: T).(getl h c0 (CHead e2 k u2)))) (\lambda (e2:
236 C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u2: T).(pr0 u1
237 u2))))))))))) (\lambda (c: C).(\lambda (h: nat).(\lambda (e1: C).(\lambda
238 (u1: T).(\lambda (k: K).(\lambda (H0: (getl h c (CHead e1 k
239 u1))).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u2: T).(getl h c (CHead e2
240 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_:
241 C).(\lambda (u2: T).(pr0 u1 u2))) e1 u1 H0 (wcpr0_refl e1) (pr0_refl
242 u1)))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (wcpr0 c3
243 c4)).(\lambda (H1: ((\forall (h: nat).(\forall (e1: C).(\forall (u1:
244 T).(\forall (k: K).((getl h c3 (CHead e1 k u1)) \to (ex3_2 C T (\lambda (e2:
245 C).(\lambda (u2: T).(getl h c4 (CHead e2 k u2)))) (\lambda (e2: C).(\lambda
246 (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u2: T).(pr0 u1
247 u2))))))))))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H2: (pr0 u1
248 u2)).(\lambda (k: K).(\lambda (h: nat).(nat_ind (\lambda (n: nat).(\forall
249 (e1: C).(\forall (u3: T).(\forall (k0: K).((getl n (CHead c3 k u1) (CHead e1
250 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(getl n (CHead c4 k
251 u2) (CHead e2 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2)))
252 (\lambda (_: C).(\lambda (u4: T).(pr0 u3 u4))))))))) (\lambda (e1:
253 C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H3: (getl O (CHead c3 k u1)
254 (CHead e1 k0 u0))).(K_ind (\lambda (k1: K).((clear (CHead c3 k1 u1) (CHead e1
255 k0 u0)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl O (CHead c4 k1
256 u2) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2)))
257 (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3)))))) (\lambda (b: B).(\lambda
258 (H4: (clear (CHead c3 (Bind b) u1) (CHead e1 k0 u0))).(let H5 \def (f_equal C
259 C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
260 \Rightarrow e1 | (CHead c _ _) \Rightarrow c])) (CHead e1 k0 u0) (CHead c3
261 (Bind b) u1) (clear_gen_bind b c3 (CHead e1 k0 u0) u1 H4)) in ((let H6 \def
262 (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with
263 [(CSort _) \Rightarrow k0 | (CHead _ k1 _) \Rightarrow k1])) (CHead e1 k0 u0)
264 (CHead c3 (Bind b) u1) (clear_gen_bind b c3 (CHead e1 k0 u0) u1 H4)) in ((let
265 H7 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
266 with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead e1 k0
267 u0) (CHead c3 (Bind b) u1) (clear_gen_bind b c3 (CHead e1 k0 u0) u1 H4)) in
268 (\lambda (H8: (eq K k0 (Bind b))).(\lambda (H9: (eq C e1 c3)).(eq_ind_r K
269 (Bind b) (\lambda (k1: K).(ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl
270 O (CHead c4 (Bind b) u2) (CHead e2 k1 u3)))) (\lambda (e2: C).(\lambda (_:
271 T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))))) (eq_ind_r
272 T u1 (\lambda (t: T).(ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl O
273 (CHead c4 (Bind b) u2) (CHead e2 (Bind b) u3)))) (\lambda (e2: C).(\lambda
274 (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 t u3)))))
275 (eq_ind_r C c3 (\lambda (c: C).(ex3_2 C T (\lambda (e2: C).(\lambda (u3:
276 T).(getl O (CHead c4 (Bind b) u2) (CHead e2 (Bind b) u3)))) (\lambda (e2:
277 C).(\lambda (_: T).(wcpr0 c e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u1
278 u3))))) (ex3_2_intro C T (\lambda (e2: C).(\lambda (u3: T).(getl O (CHead c4
279 (Bind b) u2) (CHead e2 (Bind b) u3)))) (\lambda (e2: C).(\lambda (_:
280 T).(wcpr0 c3 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u1 u3))) c4 u2
281 (getl_refl b c4 u2) H0 H2) e1 H9) u0 H7) k0 H8)))) H6)) H5)))) (\lambda (f:
282 F).(\lambda (H4: (clear (CHead c3 (Flat f) u1) (CHead e1 k0 u0))).(let H5
283 \def (H1 O e1 u0 k0 (getl_intro O c3 (CHead e1 k0 u0) c3 (drop_refl c3)
284 (clear_gen_flat f c3 (CHead e1 k0 u0) u1 H4))) in (ex3_2_ind C T (\lambda
285 (e2: C).(\lambda (u3: T).(getl O c4 (CHead e2 k0 u3)))) (\lambda (e2:
286 C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0
287 u3))) (ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl O (CHead c4 (Flat f)
288 u2) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2)))
289 (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3)))) (\lambda (x0: C).(\lambda
290 (x1: T).(\lambda (H6: (getl O c4 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 e1
291 x0)).(\lambda (H8: (pr0 u0 x1)).(ex3_2_intro C T (\lambda (e2: C).(\lambda
292 (u3: T).(getl O (CHead c4 (Flat f) u2) (CHead e2 k0 u3)))) (\lambda (e2:
293 C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0
294 u3))) x0 x1 (getl_flat c4 (CHead x0 k0 x1) O H6 f u2) H7 H8)))))) H5)))) k
295 (getl_gen_O (CHead c3 k u1) (CHead e1 k0 u0) H3)))))) (K_ind (\lambda (k0:
296 K).(\forall (n: nat).(((\forall (e1: C).(\forall (u3: T).(\forall (k1:
297 K).((getl n (CHead c3 k0 u1) (CHead e1 k1 u3)) \to (ex3_2 C T (\lambda (e2:
298 C).(\lambda (u4: T).(getl n (CHead c4 k0 u2) (CHead e2 k1 u4)))) (\lambda
299 (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u4: T).(pr0
300 u3 u4))))))))) \to (\forall (e1: C).(\forall (u3: T).(\forall (k1: K).((getl
301 (S n) (CHead c3 k0 u1) (CHead e1 k1 u3)) \to (ex3_2 C T (\lambda (e2:
302 C).(\lambda (u4: T).(getl (S n) (CHead c4 k0 u2) (CHead e2 k1 u4)))) (\lambda
303 (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u4: T).(pr0
304 u3 u4))))))))))) (\lambda (b: B).(\lambda (n: nat).(\lambda (_: ((\forall
305 (e1: C).(\forall (u3: T).(\forall (k0: K).((getl n (CHead c3 (Bind b) u1)
306 (CHead e1 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(getl n
307 (CHead c4 (Bind b) u2) (CHead e2 k0 u4)))) (\lambda (e2: C).(\lambda (_:
308 T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u4: T).(pr0 u3
309 u4)))))))))).(\lambda (e1: C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H4:
310 (getl (S n) (CHead c3 (Bind b) u1) (CHead e1 k0 u0))).(let H5 \def (H1 n e1
311 u0 k0 (getl_gen_S (Bind b) c3 (CHead e1 k0 u0) u1 n H4)) in (ex3_2_ind C T
312 (\lambda (e2: C).(\lambda (u3: T).(getl n c4 (CHead e2 k0 u3)))) (\lambda
313 (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0
314 u0 u3))) (ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl (S n) (CHead c4
315 (Bind b) u2) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1
316 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3)))) (\lambda (x0:
317 C).(\lambda (x1: T).(\lambda (H6: (getl n c4 (CHead x0 k0 x1))).(\lambda (H7:
318 (wcpr0 e1 x0)).(\lambda (H8: (pr0 u0 x1)).(ex3_2_intro C T (\lambda (e2:
319 C).(\lambda (u3: T).(getl (S n) (CHead c4 (Bind b) u2) (CHead e2 k0 u3))))
320 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda
321 (u3: T).(pr0 u0 u3))) x0 x1 (getl_head (Bind b) n c4 (CHead x0 k0 x1) H6 u2)
322 H7 H8)))))) H5))))))))) (\lambda (f: F).(\lambda (n: nat).(\lambda (_:
323 ((\forall (e1: C).(\forall (u3: T).(\forall (k0: K).((getl n (CHead c3 (Flat
324 f) u1) (CHead e1 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4:
325 T).(getl n (CHead c4 (Flat f) u2) (CHead e2 k0 u4)))) (\lambda (e2:
326 C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u4: T).(pr0 u3
327 u4)))))))))).(\lambda (e1: C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H4:
328 (getl (S n) (CHead c3 (Flat f) u1) (CHead e1 k0 u0))).(let H5 \def (H1 (S n)
329 e1 u0 k0 (getl_gen_S (Flat f) c3 (CHead e1 k0 u0) u1 n H4)) in (ex3_2_ind C T
330 (\lambda (e2: C).(\lambda (u3: T).(getl (S n) c4 (CHead e2 k0 u3)))) (\lambda
331 (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0
332 u0 u3))) (ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl (S n) (CHead c4
333 (Flat f) u2) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1
334 e2))) (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3)))) (\lambda (x0:
335 C).(\lambda (x1: T).(\lambda (H6: (getl (S n) c4 (CHead x0 k0 x1))).(\lambda
336 (H7: (wcpr0 e1 x0)).(\lambda (H8: (pr0 u0 x1)).(ex3_2_intro C T (\lambda (e2:
337 C).(\lambda (u3: T).(getl (S n) (CHead c4 (Flat f) u2) (CHead e2 k0 u3))))
338 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda
339 (u3: T).(pr0 u0 u3))) x0 x1 (getl_head (Flat f) n c4 (CHead x0 k0 x1) H6 u2)
340 H7 H8)))))) H5))))))))) k) h)))))))))) c1 c2 H))).
345 theorem wcpr0_getl_back:
346 \forall (c1: C).(\forall (c2: C).((wcpr0 c2 c1) \to (\forall (h:
347 nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((getl h c1 (CHead e1
348 k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(getl h c2 (CHead e2
349 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_:
350 C).(\lambda (u2: T).(pr0 u2 u1)))))))))))
352 \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (wcpr0 c2 c1)).(wcpr0_ind
353 (\lambda (c: C).(\lambda (c0: C).(\forall (h: nat).(\forall (e1: C).(\forall
354 (u1: T).(\forall (k: K).((getl h c0 (CHead e1 k u1)) \to (ex3_2 C T (\lambda
355 (e2: C).(\lambda (u2: T).(getl h c (CHead e2 k u2)))) (\lambda (e2:
356 C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u2: T).(pr0 u2
357 u1))))))))))) (\lambda (c: C).(\lambda (h: nat).(\lambda (e1: C).(\lambda
358 (u1: T).(\lambda (k: K).(\lambda (H0: (getl h c (CHead e1 k
359 u1))).(ex3_2_intro C T (\lambda (e2: C).(\lambda (u2: T).(getl h c (CHead e2
360 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_:
361 C).(\lambda (u2: T).(pr0 u2 u1))) e1 u1 H0 (wcpr0_refl e1) (pr0_refl
362 u1)))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (wcpr0 c3
363 c4)).(\lambda (H1: ((\forall (h: nat).(\forall (e1: C).(\forall (u1:
364 T).(\forall (k: K).((getl h c4 (CHead e1 k u1)) \to (ex3_2 C T (\lambda (e2:
365 C).(\lambda (u2: T).(getl h c3 (CHead e2 k u2)))) (\lambda (e2: C).(\lambda
366 (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u2: T).(pr0 u2
367 u1))))))))))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H2: (pr0 u1
368 u2)).(\lambda (k: K).(\lambda (h: nat).(nat_ind (\lambda (n: nat).(\forall
369 (e1: C).(\forall (u3: T).(\forall (k0: K).((getl n (CHead c4 k u2) (CHead e1
370 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(getl n (CHead c3 k
371 u1) (CHead e2 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1)))
372 (\lambda (_: C).(\lambda (u4: T).(pr0 u4 u3))))))))) (\lambda (e1:
373 C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H3: (getl O (CHead c4 k u2)
374 (CHead e1 k0 u0))).(K_ind (\lambda (k1: K).((clear (CHead c4 k1 u2) (CHead e1
375 k0 u0)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl O (CHead c3 k1
376 u1) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1)))
377 (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0)))))) (\lambda (b: B).(\lambda
378 (H4: (clear (CHead c4 (Bind b) u2) (CHead e1 k0 u0))).(let H5 \def (f_equal C
379 C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
380 \Rightarrow e1 | (CHead c _ _) \Rightarrow c])) (CHead e1 k0 u0) (CHead c4
381 (Bind b) u2) (clear_gen_bind b c4 (CHead e1 k0 u0) u2 H4)) in ((let H6 \def
382 (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with
383 [(CSort _) \Rightarrow k0 | (CHead _ k1 _) \Rightarrow k1])) (CHead e1 k0 u0)
384 (CHead c4 (Bind b) u2) (clear_gen_bind b c4 (CHead e1 k0 u0) u2 H4)) in ((let
385 H7 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
386 with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead e1 k0
387 u0) (CHead c4 (Bind b) u2) (clear_gen_bind b c4 (CHead e1 k0 u0) u2 H4)) in
388 (\lambda (H8: (eq K k0 (Bind b))).(\lambda (H9: (eq C e1 c4)).(eq_ind_r K
389 (Bind b) (\lambda (k1: K).(ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl
390 O (CHead c3 (Bind b) u1) (CHead e2 k1 u3)))) (\lambda (e2: C).(\lambda (_:
391 T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))))) (eq_ind_r
392 T u2 (\lambda (t: T).(ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl O
393 (CHead c3 (Bind b) u1) (CHead e2 (Bind b) u3)))) (\lambda (e2: C).(\lambda
394 (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 t)))))
395 (eq_ind_r C c4 (\lambda (c: C).(ex3_2 C T (\lambda (e2: C).(\lambda (u3:
396 T).(getl O (CHead c3 (Bind b) u1) (CHead e2 (Bind b) u3)))) (\lambda (e2:
397 C).(\lambda (_: T).(wcpr0 e2 c))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3
398 u2))))) (ex3_2_intro C T (\lambda (e2: C).(\lambda (u3: T).(getl O (CHead c3
399 (Bind b) u1) (CHead e2 (Bind b) u3)))) (\lambda (e2: C).(\lambda (_:
400 T).(wcpr0 e2 c4))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u2))) c3 u1
401 (getl_refl b c3 u1) H0 H2) e1 H9) u0 H7) k0 H8)))) H6)) H5)))) (\lambda (f:
402 F).(\lambda (H4: (clear (CHead c4 (Flat f) u2) (CHead e1 k0 u0))).(let H5
403 \def (H1 O e1 u0 k0 (getl_intro O c4 (CHead e1 k0 u0) c4 (drop_refl c4)
404 (clear_gen_flat f c4 (CHead e1 k0 u0) u2 H4))) in (ex3_2_ind C T (\lambda
405 (e2: C).(\lambda (u3: T).(getl O c3 (CHead e2 k0 u3)))) (\lambda (e2:
406 C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3
407 u0))) (ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl O (CHead c3 (Flat f)
408 u1) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1)))
409 (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0)))) (\lambda (x0: C).(\lambda
410 (x1: T).(\lambda (H6: (getl O c3 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 x0
411 e1)).(\lambda (H8: (pr0 x1 u0)).(ex3_2_intro C T (\lambda (e2: C).(\lambda
412 (u3: T).(getl O (CHead c3 (Flat f) u1) (CHead e2 k0 u3)))) (\lambda (e2:
413 C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3
414 u0))) x0 x1 (getl_flat c3 (CHead x0 k0 x1) O H6 f u1) H7 H8)))))) H5)))) k
415 (getl_gen_O (CHead c4 k u2) (CHead e1 k0 u0) H3)))))) (K_ind (\lambda (k0:
416 K).(\forall (n: nat).(((\forall (e1: C).(\forall (u3: T).(\forall (k1:
417 K).((getl n (CHead c4 k0 u2) (CHead e1 k1 u3)) \to (ex3_2 C T (\lambda (e2:
418 C).(\lambda (u4: T).(getl n (CHead c3 k0 u1) (CHead e2 k1 u4)))) (\lambda
419 (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u4: T).(pr0
420 u4 u3))))))))) \to (\forall (e1: C).(\forall (u3: T).(\forall (k1: K).((getl
421 (S n) (CHead c4 k0 u2) (CHead e1 k1 u3)) \to (ex3_2 C T (\lambda (e2:
422 C).(\lambda (u4: T).(getl (S n) (CHead c3 k0 u1) (CHead e2 k1 u4)))) (\lambda
423 (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u4: T).(pr0
424 u4 u3))))))))))) (\lambda (b: B).(\lambda (n: nat).(\lambda (_: ((\forall
425 (e1: C).(\forall (u3: T).(\forall (k0: K).((getl n (CHead c4 (Bind b) u2)
426 (CHead e1 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(getl n
427 (CHead c3 (Bind b) u1) (CHead e2 k0 u4)))) (\lambda (e2: C).(\lambda (_:
428 T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u4: T).(pr0 u4
429 u3)))))))))).(\lambda (e1: C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H4:
430 (getl (S n) (CHead c4 (Bind b) u2) (CHead e1 k0 u0))).(let H5 \def (H1 n e1
431 u0 k0 (getl_gen_S (Bind b) c4 (CHead e1 k0 u0) u2 n H4)) in (ex3_2_ind C T
432 (\lambda (e2: C).(\lambda (u3: T).(getl n c3 (CHead e2 k0 u3)))) (\lambda
433 (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0
434 u3 u0))) (ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl (S n) (CHead c3
435 (Bind b) u1) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2
436 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0)))) (\lambda (x0:
437 C).(\lambda (x1: T).(\lambda (H6: (getl n c3 (CHead x0 k0 x1))).(\lambda (H7:
438 (wcpr0 x0 e1)).(\lambda (H8: (pr0 x1 u0)).(ex3_2_intro C T (\lambda (e2:
439 C).(\lambda (u3: T).(getl (S n) (CHead c3 (Bind b) u1) (CHead e2 k0 u3))))
440 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda
441 (u3: T).(pr0 u3 u0))) x0 x1 (getl_head (Bind b) n c3 (CHead x0 k0 x1) H6 u1)
442 H7 H8)))))) H5))))))))) (\lambda (f: F).(\lambda (n: nat).(\lambda (_:
443 ((\forall (e1: C).(\forall (u3: T).(\forall (k0: K).((getl n (CHead c4 (Flat
444 f) u2) (CHead e1 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4:
445 T).(getl n (CHead c3 (Flat f) u1) (CHead e2 k0 u4)))) (\lambda (e2:
446 C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u4: T).(pr0 u4
447 u3)))))))))).(\lambda (e1: C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H4:
448 (getl (S n) (CHead c4 (Flat f) u2) (CHead e1 k0 u0))).(let H5 \def (H1 (S n)
449 e1 u0 k0 (getl_gen_S (Flat f) c4 (CHead e1 k0 u0) u2 n H4)) in (ex3_2_ind C T
450 (\lambda (e2: C).(\lambda (u3: T).(getl (S n) c3 (CHead e2 k0 u3)))) (\lambda
451 (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0
452 u3 u0))) (ex3_2 C T (\lambda (e2: C).(\lambda (u3: T).(getl (S n) (CHead c3
453 (Flat f) u1) (CHead e2 k0 u3)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2
454 e1))) (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0)))) (\lambda (x0:
455 C).(\lambda (x1: T).(\lambda (H6: (getl (S n) c3 (CHead x0 k0 x1))).(\lambda
456 (H7: (wcpr0 x0 e1)).(\lambda (H8: (pr0 x1 u0)).(ex3_2_intro C T (\lambda (e2:
457 C).(\lambda (u3: T).(getl (S n) (CHead c3 (Flat f) u1) (CHead e2 k0 u3))))
458 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda
459 (u3: T).(pr0 u3 u0))) x0 x1 (getl_head (Flat f) n c3 (CHead x0 k0 x1) H6 u1)
460 H7 H8)))))) H5))))))))) k) h)))))))))) c2 c1 H))).