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/fwd.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)).(let TMP_5 \def
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 (let TMP_2 \def
31 (\lambda (e2: C).(\lambda (u2: T).(let TMP_1 \def (CHead e2 k u2) in (drop h
32 O c0 TMP_1)))) in (let TMP_3 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1
33 e2))) in (let TMP_4 \def (\lambda (_: C).(\lambda (u2: T).(pr0 u1 u2))) in
34 (ex3_2 C T TMP_2 TMP_3 TMP_4))))))))))) in (let TMP_12 \def (\lambda (c:
35 C).(\lambda (h: nat).(\lambda (e1: C).(\lambda (u1: T).(\lambda (k:
36 K).(\lambda (H0: (drop h O c (CHead e1 k u1))).(let TMP_7 \def (\lambda (e2:
37 C).(\lambda (u2: T).(let TMP_6 \def (CHead e2 k u2) in (drop h O c TMP_6))))
38 in (let TMP_8 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) in (let
39 TMP_9 \def (\lambda (_: C).(\lambda (u2: T).(pr0 u1 u2))) in (let TMP_10 \def
40 (wcpr0_refl e1) in (let TMP_11 \def (pr0_refl u1) in (ex3_2_intro C T TMP_7
41 TMP_8 TMP_9 e1 u1 H0 TMP_10 TMP_11)))))))))))) in (let TMP_132 \def (\lambda
42 (c3: C).(\lambda (c4: C).(\lambda (H0: (wcpr0 c3 c4)).(\lambda (H1: ((\forall
43 (h: nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((drop h O c3
44 (CHead e1 k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(drop h O
45 c4 (CHead e2 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2)))
46 (\lambda (_: C).(\lambda (u2: T).(pr0 u1 u2))))))))))).(\lambda (u1:
47 T).(\lambda (u2: T).(\lambda (H2: (pr0 u1 u2)).(\lambda (k: K).(\lambda (h:
48 nat).(let TMP_18 \def (\lambda (n: nat).(\forall (e1: C).(\forall (u3:
49 T).(\forall (k0: K).((drop n O (CHead c3 k u1) (CHead e1 k0 u3)) \to (let
50 TMP_15 \def (\lambda (e2: C).(\lambda (u4: T).(let TMP_13 \def (CHead c4 k
51 u2) in (let TMP_14 \def (CHead e2 k0 u4) in (drop n O TMP_13 TMP_14))))) in
52 (let TMP_16 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) in (let
53 TMP_17 \def (\lambda (_: C).(\lambda (u4: T).(pr0 u3 u4))) in (ex3_2 C T
54 TMP_15 TMP_16 TMP_17))))))))) in (let TMP_67 \def (\lambda (e1: C).(\lambda
55 (u0: T).(\lambda (k0: K).(\lambda (H3: (drop O O (CHead c3 k u1) (CHead e1 k0
56 u0))).(let TMP_19 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow
57 c3 | (CHead c _ _) \Rightarrow c])) in (let TMP_20 \def (CHead c3 k u1) in
58 (let TMP_21 \def (CHead e1 k0 u0) in (let TMP_22 \def (CHead c3 k u1) in (let
59 TMP_23 \def (CHead e1 k0 u0) in (let TMP_24 \def (drop_gen_refl TMP_22 TMP_23
60 H3) in (let H4 \def (f_equal C C TMP_19 TMP_20 TMP_21 TMP_24) in (let TMP_25
61 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow k | (CHead _ k1 _)
62 \Rightarrow k1])) in (let TMP_26 \def (CHead c3 k u1) in (let TMP_27 \def
63 (CHead e1 k0 u0) in (let TMP_28 \def (CHead c3 k u1) in (let TMP_29 \def
64 (CHead e1 k0 u0) in (let TMP_30 \def (drop_gen_refl TMP_28 TMP_29 H3) in (let
65 H5 \def (f_equal C K TMP_25 TMP_26 TMP_27 TMP_30) in (let TMP_31 \def
66 (\lambda (e: C).(match e with [(CSort _) \Rightarrow u1 | (CHead _ _ t)
67 \Rightarrow t])) in (let TMP_32 \def (CHead c3 k u1) in (let TMP_33 \def
68 (CHead e1 k0 u0) in (let TMP_34 \def (CHead c3 k u1) in (let TMP_35 \def
69 (CHead e1 k0 u0) in (let TMP_36 \def (drop_gen_refl TMP_34 TMP_35 H3) in (let
70 H6 \def (f_equal C T TMP_31 TMP_32 TMP_33 TMP_36) in (let TMP_65 \def
71 (\lambda (H7: (eq K k k0)).(\lambda (H8: (eq C c3 e1)).(let TMP_42 \def
72 (\lambda (k1: K).(let TMP_39 \def (\lambda (e2: C).(\lambda (u3: T).(let
73 TMP_37 \def (CHead c4 k u2) in (let TMP_38 \def (CHead e2 k1 u3) in (drop O O
74 TMP_37 TMP_38))))) in (let TMP_40 \def (\lambda (e2: C).(\lambda (_:
75 T).(wcpr0 e1 e2))) in (let TMP_41 \def (\lambda (_: C).(\lambda (u3: T).(pr0
76 u0 u3))) in (ex3_2 C T TMP_39 TMP_40 TMP_41))))) in (let TMP_48 \def (\lambda
77 (t: T).(let TMP_45 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_43 \def
78 (CHead c4 k u2) in (let TMP_44 \def (CHead e2 k u3) in (drop O O TMP_43
79 TMP_44))))) in (let TMP_46 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1
80 e2))) in (let TMP_47 \def (\lambda (_: C).(\lambda (u3: T).(pr0 t u3))) in
81 (ex3_2 C T TMP_45 TMP_46 TMP_47))))) in (let TMP_54 \def (\lambda (c: C).(let
82 TMP_51 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_49 \def (CHead c4 k
83 u2) in (let TMP_50 \def (CHead e2 k u3) in (drop O O TMP_49 TMP_50))))) in
84 (let TMP_52 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 c e2))) in (let
85 TMP_53 \def (\lambda (_: C).(\lambda (u3: T).(pr0 u1 u3))) in (ex3_2 C T
86 TMP_51 TMP_52 TMP_53))))) in (let TMP_57 \def (\lambda (e2: C).(\lambda (u3:
87 T).(let TMP_55 \def (CHead c4 k u2) in (let TMP_56 \def (CHead e2 k u3) in
88 (drop O O TMP_55 TMP_56))))) in (let TMP_58 \def (\lambda (e2: C).(\lambda
89 (_: T).(wcpr0 c3 e2))) in (let TMP_59 \def (\lambda (_: C).(\lambda (u3:
90 T).(pr0 u1 u3))) in (let TMP_60 \def (CHead c4 k u2) in (let TMP_61 \def
91 (drop_refl TMP_60) in (let TMP_62 \def (ex3_2_intro C T TMP_57 TMP_58 TMP_59
92 c4 u2 TMP_61 H0 H2) in (let TMP_63 \def (eq_ind C c3 TMP_54 TMP_62 e1 H8) in
93 (let TMP_64 \def (eq_ind T u1 TMP_48 TMP_63 u0 H6) in (eq_ind K k TMP_42
94 TMP_64 k0 H7)))))))))))))) in (let TMP_66 \def (TMP_65 H5) in (TMP_66
95 H4)))))))))))))))))))))))))))) in (let TMP_74 \def (\lambda (k0: K).(\forall
96 (n: nat).(((\forall (e1: C).(\forall (u3: T).(\forall (k1: K).((drop n O
97 (CHead c3 k0 u1) (CHead e1 k1 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda
98 (u4: T).(drop n O (CHead c4 k0 u2) (CHead e2 k1 u4)))) (\lambda (e2:
99 C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u4: T).(pr0 u3
100 u4))))))))) \to (\forall (e1: C).(\forall (u3: T).(\forall (k1: K).((drop (S
101 n) O (CHead c3 k0 u1) (CHead e1 k1 u3)) \to (let TMP_71 \def (\lambda (e2:
102 C).(\lambda (u4: T).(let TMP_68 \def (S n) in (let TMP_69 \def (CHead c4 k0
103 u2) in (let TMP_70 \def (CHead e2 k1 u4) in (drop TMP_68 O TMP_69
104 TMP_70)))))) in (let TMP_72 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1
105 e2))) in (let TMP_73 \def (\lambda (_: C).(\lambda (u4: T).(pr0 u3 u4))) in
106 (ex3_2 C T TMP_71 TMP_72 TMP_73))))))))))) in (let TMP_101 \def (\lambda (b:
107 B).(\lambda (n: nat).(\lambda (_: ((\forall (e1: C).(\forall (u3: T).(\forall
108 (k0: K).((drop n O (CHead c3 (Bind b) u1) (CHead e1 k0 u3)) \to (ex3_2 C T
109 (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead c4 (Bind b) u2) (CHead e2
110 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_:
111 C).(\lambda (u4: T).(pr0 u3 u4)))))))))).(\lambda (e1: C).(\lambda (u0:
112 T).(\lambda (k0: K).(\lambda (H4: (drop (S n) O (CHead c3 (Bind b) u1) (CHead
113 e1 k0 u0))).(let TMP_75 \def (Bind b) in (let TMP_76 \def (CHead e1 k0 u0) in
114 (let TMP_77 \def (drop_gen_drop TMP_75 c3 TMP_76 u1 n H4) in (let H5 \def (H1
115 n e1 u0 k0 TMP_77) in (let TMP_79 \def (\lambda (e2: C).(\lambda (u3: T).(let
116 TMP_78 \def (CHead e2 k0 u3) in (drop n O c4 TMP_78)))) in (let TMP_80 \def
117 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) in (let TMP_81 \def (\lambda
118 (_: C).(\lambda (u3: T).(pr0 u0 u3))) in (let TMP_86 \def (\lambda (e2:
119 C).(\lambda (u3: T).(let TMP_82 \def (S n) in (let TMP_83 \def (Bind b) in
120 (let TMP_84 \def (CHead c4 TMP_83 u2) in (let TMP_85 \def (CHead e2 k0 u3) in
121 (drop TMP_82 O TMP_84 TMP_85))))))) in (let TMP_87 \def (\lambda (e2:
122 C).(\lambda (_: T).(wcpr0 e1 e2))) in (let TMP_88 \def (\lambda (_:
123 C).(\lambda (u3: T).(pr0 u0 u3))) in (let TMP_89 \def (ex3_2 C T TMP_86
124 TMP_87 TMP_88) in (let TMP_100 \def (\lambda (x0: C).(\lambda (x1:
125 T).(\lambda (H6: (drop n O c4 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 e1
126 x0)).(\lambda (H8: (pr0 u0 x1)).(let TMP_94 \def (\lambda (e2: C).(\lambda
127 (u3: T).(let TMP_90 \def (S n) in (let TMP_91 \def (Bind b) in (let TMP_92
128 \def (CHead c4 TMP_91 u2) in (let TMP_93 \def (CHead e2 k0 u3) in (drop
129 TMP_90 O TMP_92 TMP_93))))))) in (let TMP_95 \def (\lambda (e2: C).(\lambda
130 (_: T).(wcpr0 e1 e2))) in (let TMP_96 \def (\lambda (_: C).(\lambda (u3:
131 T).(pr0 u0 u3))) in (let TMP_97 \def (Bind b) in (let TMP_98 \def (CHead x0
132 k0 x1) in (let TMP_99 \def (drop_drop TMP_97 n c4 TMP_98 H6 u2) in
133 (ex3_2_intro C T TMP_94 TMP_95 TMP_96 x0 x1 TMP_99 H7 H8)))))))))))) in
134 (ex3_2_ind C T TMP_79 TMP_80 TMP_81 TMP_89 TMP_100 H5)))))))))))))))))))) in
135 (let TMP_130 \def (\lambda (f: F).(\lambda (n: nat).(\lambda (_: ((\forall
136 (e1: C).(\forall (u3: T).(\forall (k0: K).((drop n O (CHead c3 (Flat f) u1)
137 (CHead e1 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(drop n O
138 (CHead c4 (Flat f) u2) (CHead e2 k0 u4)))) (\lambda (e2: C).(\lambda (_:
139 T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u4: T).(pr0 u3
140 u4)))))))))).(\lambda (e1: C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H4:
141 (drop (S n) O (CHead c3 (Flat f) u1) (CHead e1 k0 u0))).(let TMP_102 \def (S
142 n) in (let TMP_103 \def (Flat f) in (let TMP_104 \def (CHead e1 k0 u0) in
143 (let TMP_105 \def (drop_gen_drop TMP_103 c3 TMP_104 u1 n H4) in (let H5 \def
144 (H1 TMP_102 e1 u0 k0 TMP_105) in (let TMP_108 \def (\lambda (e2: C).(\lambda
145 (u3: T).(let TMP_106 \def (S n) in (let TMP_107 \def (CHead e2 k0 u3) in
146 (drop TMP_106 O c4 TMP_107))))) in (let TMP_109 \def (\lambda (e2:
147 C).(\lambda (_: T).(wcpr0 e1 e2))) in (let TMP_110 \def (\lambda (_:
148 C).(\lambda (u3: T).(pr0 u0 u3))) in (let TMP_115 \def (\lambda (e2:
149 C).(\lambda (u3: T).(let TMP_111 \def (S n) in (let TMP_112 \def (Flat f) in
150 (let TMP_113 \def (CHead c4 TMP_112 u2) in (let TMP_114 \def (CHead e2 k0 u3)
151 in (drop TMP_111 O TMP_113 TMP_114))))))) in (let TMP_116 \def (\lambda (e2:
152 C).(\lambda (_: T).(wcpr0 e1 e2))) in (let TMP_117 \def (\lambda (_:
153 C).(\lambda (u3: T).(pr0 u0 u3))) in (let TMP_118 \def (ex3_2 C T TMP_115
154 TMP_116 TMP_117) in (let TMP_129 \def (\lambda (x0: C).(\lambda (x1:
155 T).(\lambda (H6: (drop (S n) O c4 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 e1
156 x0)).(\lambda (H8: (pr0 u0 x1)).(let TMP_123 \def (\lambda (e2: C).(\lambda
157 (u3: T).(let TMP_119 \def (S n) in (let TMP_120 \def (Flat f) in (let TMP_121
158 \def (CHead c4 TMP_120 u2) in (let TMP_122 \def (CHead e2 k0 u3) in (drop
159 TMP_119 O TMP_121 TMP_122))))))) in (let TMP_124 \def (\lambda (e2:
160 C).(\lambda (_: T).(wcpr0 e1 e2))) in (let TMP_125 \def (\lambda (_:
161 C).(\lambda (u3: T).(pr0 u0 u3))) in (let TMP_126 \def (Flat f) in (let
162 TMP_127 \def (CHead x0 k0 x1) in (let TMP_128 \def (drop_drop TMP_126 n c4
163 TMP_127 H6 u2) in (ex3_2_intro C T TMP_123 TMP_124 TMP_125 x0 x1 TMP_128 H7
164 H8)))))))))))) in (ex3_2_ind C T TMP_108 TMP_109 TMP_110 TMP_118 TMP_129
165 H5))))))))))))))))))))) in (let TMP_131 \def (K_ind TMP_74 TMP_101 TMP_130 k)
166 in (nat_ind TMP_18 TMP_67 TMP_131 h)))))))))))))))) in (wcpr0_ind TMP_5
167 TMP_12 TMP_132 c1 c2 H)))))).
169 theorem wcpr0_drop_back:
170 \forall (c1: C).(\forall (c2: C).((wcpr0 c2 c1) \to (\forall (h:
171 nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((drop h O c1 (CHead
172 e1 k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(drop h O c2
173 (CHead e2 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda
174 (_: C).(\lambda (u2: T).(pr0 u2 u1)))))))))))
176 \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (wcpr0 c2 c1)).(let TMP_5 \def
177 (\lambda (c: C).(\lambda (c0: C).(\forall (h: nat).(\forall (e1: C).(\forall
178 (u1: T).(\forall (k: K).((drop h O c0 (CHead e1 k u1)) \to (let TMP_2 \def
179 (\lambda (e2: C).(\lambda (u2: T).(let TMP_1 \def (CHead e2 k u2) in (drop h
180 O c TMP_1)))) in (let TMP_3 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2
181 e1))) in (let TMP_4 \def (\lambda (_: C).(\lambda (u2: T).(pr0 u2 u1))) in
182 (ex3_2 C T TMP_2 TMP_3 TMP_4))))))))))) in (let TMP_12 \def (\lambda (c:
183 C).(\lambda (h: nat).(\lambda (e1: C).(\lambda (u1: T).(\lambda (k:
184 K).(\lambda (H0: (drop h O c (CHead e1 k u1))).(let TMP_7 \def (\lambda (e2:
185 C).(\lambda (u2: T).(let TMP_6 \def (CHead e2 k u2) in (drop h O c TMP_6))))
186 in (let TMP_8 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) in (let
187 TMP_9 \def (\lambda (_: C).(\lambda (u2: T).(pr0 u2 u1))) in (let TMP_10 \def
188 (wcpr0_refl e1) in (let TMP_11 \def (pr0_refl u1) in (ex3_2_intro C T TMP_7
189 TMP_8 TMP_9 e1 u1 H0 TMP_10 TMP_11)))))))))))) in (let TMP_132 \def (\lambda
190 (c3: C).(\lambda (c4: C).(\lambda (H0: (wcpr0 c3 c4)).(\lambda (H1: ((\forall
191 (h: nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((drop h O c4
192 (CHead e1 k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(drop h O
193 c3 (CHead e2 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1)))
194 (\lambda (_: C).(\lambda (u2: T).(pr0 u2 u1))))))))))).(\lambda (u1:
195 T).(\lambda (u2: T).(\lambda (H2: (pr0 u1 u2)).(\lambda (k: K).(\lambda (h:
196 nat).(let TMP_18 \def (\lambda (n: nat).(\forall (e1: C).(\forall (u3:
197 T).(\forall (k0: K).((drop n O (CHead c4 k u2) (CHead e1 k0 u3)) \to (let
198 TMP_15 \def (\lambda (e2: C).(\lambda (u4: T).(let TMP_13 \def (CHead c3 k
199 u1) in (let TMP_14 \def (CHead e2 k0 u4) in (drop n O TMP_13 TMP_14))))) in
200 (let TMP_16 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) in (let
201 TMP_17 \def (\lambda (_: C).(\lambda (u4: T).(pr0 u4 u3))) in (ex3_2 C T
202 TMP_15 TMP_16 TMP_17))))))))) in (let TMP_67 \def (\lambda (e1: C).(\lambda
203 (u0: T).(\lambda (k0: K).(\lambda (H3: (drop O O (CHead c4 k u2) (CHead e1 k0
204 u0))).(let TMP_19 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow
205 c4 | (CHead c _ _) \Rightarrow c])) in (let TMP_20 \def (CHead c4 k u2) in
206 (let TMP_21 \def (CHead e1 k0 u0) in (let TMP_22 \def (CHead c4 k u2) in (let
207 TMP_23 \def (CHead e1 k0 u0) in (let TMP_24 \def (drop_gen_refl TMP_22 TMP_23
208 H3) in (let H4 \def (f_equal C C TMP_19 TMP_20 TMP_21 TMP_24) in (let TMP_25
209 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow k | (CHead _ k1 _)
210 \Rightarrow k1])) in (let TMP_26 \def (CHead c4 k u2) in (let TMP_27 \def
211 (CHead e1 k0 u0) in (let TMP_28 \def (CHead c4 k u2) in (let TMP_29 \def
212 (CHead e1 k0 u0) in (let TMP_30 \def (drop_gen_refl TMP_28 TMP_29 H3) in (let
213 H5 \def (f_equal C K TMP_25 TMP_26 TMP_27 TMP_30) in (let TMP_31 \def
214 (\lambda (e: C).(match e with [(CSort _) \Rightarrow u2 | (CHead _ _ t)
215 \Rightarrow t])) in (let TMP_32 \def (CHead c4 k u2) in (let TMP_33 \def
216 (CHead e1 k0 u0) in (let TMP_34 \def (CHead c4 k u2) in (let TMP_35 \def
217 (CHead e1 k0 u0) in (let TMP_36 \def (drop_gen_refl TMP_34 TMP_35 H3) in (let
218 H6 \def (f_equal C T TMP_31 TMP_32 TMP_33 TMP_36) in (let TMP_65 \def
219 (\lambda (H7: (eq K k k0)).(\lambda (H8: (eq C c4 e1)).(let TMP_42 \def
220 (\lambda (k1: K).(let TMP_39 \def (\lambda (e2: C).(\lambda (u3: T).(let
221 TMP_37 \def (CHead c3 k u1) in (let TMP_38 \def (CHead e2 k1 u3) in (drop O O
222 TMP_37 TMP_38))))) in (let TMP_40 \def (\lambda (e2: C).(\lambda (_:
223 T).(wcpr0 e2 e1))) in (let TMP_41 \def (\lambda (_: C).(\lambda (u3: T).(pr0
224 u3 u0))) in (ex3_2 C T TMP_39 TMP_40 TMP_41))))) in (let TMP_48 \def (\lambda
225 (t: T).(let TMP_45 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_43 \def
226 (CHead c3 k u1) in (let TMP_44 \def (CHead e2 k u3) in (drop O O TMP_43
227 TMP_44))))) in (let TMP_46 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2
228 e1))) in (let TMP_47 \def (\lambda (_: C).(\lambda (u3: T).(pr0 u3 t))) in
229 (ex3_2 C T TMP_45 TMP_46 TMP_47))))) in (let TMP_54 \def (\lambda (c: C).(let
230 TMP_51 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_49 \def (CHead c3 k
231 u1) in (let TMP_50 \def (CHead e2 k u3) in (drop O O TMP_49 TMP_50))))) in
232 (let TMP_52 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 c))) in (let
233 TMP_53 \def (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u2))) in (ex3_2 C T
234 TMP_51 TMP_52 TMP_53))))) in (let TMP_57 \def (\lambda (e2: C).(\lambda (u3:
235 T).(let TMP_55 \def (CHead c3 k u1) in (let TMP_56 \def (CHead e2 k u3) in
236 (drop O O TMP_55 TMP_56))))) in (let TMP_58 \def (\lambda (e2: C).(\lambda
237 (_: T).(wcpr0 e2 c4))) in (let TMP_59 \def (\lambda (_: C).(\lambda (u3:
238 T).(pr0 u3 u2))) in (let TMP_60 \def (CHead c3 k u1) in (let TMP_61 \def
239 (drop_refl TMP_60) in (let TMP_62 \def (ex3_2_intro C T TMP_57 TMP_58 TMP_59
240 c3 u1 TMP_61 H0 H2) in (let TMP_63 \def (eq_ind C c4 TMP_54 TMP_62 e1 H8) in
241 (let TMP_64 \def (eq_ind T u2 TMP_48 TMP_63 u0 H6) in (eq_ind K k TMP_42
242 TMP_64 k0 H7)))))))))))))) in (let TMP_66 \def (TMP_65 H5) in (TMP_66
243 H4)))))))))))))))))))))))))))) in (let TMP_74 \def (\lambda (k0: K).(\forall
244 (n: nat).(((\forall (e1: C).(\forall (u3: T).(\forall (k1: K).((drop n O
245 (CHead c4 k0 u2) (CHead e1 k1 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda
246 (u4: T).(drop n O (CHead c3 k0 u1) (CHead e2 k1 u4)))) (\lambda (e2:
247 C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u4: T).(pr0 u4
248 u3))))))))) \to (\forall (e1: C).(\forall (u3: T).(\forall (k1: K).((drop (S
249 n) O (CHead c4 k0 u2) (CHead e1 k1 u3)) \to (let TMP_71 \def (\lambda (e2:
250 C).(\lambda (u4: T).(let TMP_68 \def (S n) in (let TMP_69 \def (CHead c3 k0
251 u1) in (let TMP_70 \def (CHead e2 k1 u4) in (drop TMP_68 O TMP_69
252 TMP_70)))))) in (let TMP_72 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2
253 e1))) in (let TMP_73 \def (\lambda (_: C).(\lambda (u4: T).(pr0 u4 u3))) in
254 (ex3_2 C T TMP_71 TMP_72 TMP_73))))))))))) in (let TMP_101 \def (\lambda (b:
255 B).(\lambda (n: nat).(\lambda (_: ((\forall (e1: C).(\forall (u3: T).(\forall
256 (k0: K).((drop n O (CHead c4 (Bind b) u2) (CHead e1 k0 u3)) \to (ex3_2 C T
257 (\lambda (e2: C).(\lambda (u4: T).(drop n O (CHead c3 (Bind b) u1) (CHead e2
258 k0 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_:
259 C).(\lambda (u4: T).(pr0 u4 u3)))))))))).(\lambda (e1: C).(\lambda (u0:
260 T).(\lambda (k0: K).(\lambda (H4: (drop (S n) O (CHead c4 (Bind b) u2) (CHead
261 e1 k0 u0))).(let TMP_75 \def (Bind b) in (let TMP_76 \def (CHead e1 k0 u0) in
262 (let TMP_77 \def (drop_gen_drop TMP_75 c4 TMP_76 u2 n H4) in (let H5 \def (H1
263 n e1 u0 k0 TMP_77) in (let TMP_79 \def (\lambda (e2: C).(\lambda (u3: T).(let
264 TMP_78 \def (CHead e2 k0 u3) in (drop n O c3 TMP_78)))) in (let TMP_80 \def
265 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) in (let TMP_81 \def (\lambda
266 (_: C).(\lambda (u3: T).(pr0 u3 u0))) in (let TMP_86 \def (\lambda (e2:
267 C).(\lambda (u3: T).(let TMP_82 \def (S n) in (let TMP_83 \def (Bind b) in
268 (let TMP_84 \def (CHead c3 TMP_83 u1) in (let TMP_85 \def (CHead e2 k0 u3) in
269 (drop TMP_82 O TMP_84 TMP_85))))))) in (let TMP_87 \def (\lambda (e2:
270 C).(\lambda (_: T).(wcpr0 e2 e1))) in (let TMP_88 \def (\lambda (_:
271 C).(\lambda (u3: T).(pr0 u3 u0))) in (let TMP_89 \def (ex3_2 C T TMP_86
272 TMP_87 TMP_88) in (let TMP_100 \def (\lambda (x0: C).(\lambda (x1:
273 T).(\lambda (H6: (drop n O c3 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 x0
274 e1)).(\lambda (H8: (pr0 x1 u0)).(let TMP_94 \def (\lambda (e2: C).(\lambda
275 (u3: T).(let TMP_90 \def (S n) in (let TMP_91 \def (Bind b) in (let TMP_92
276 \def (CHead c3 TMP_91 u1) in (let TMP_93 \def (CHead e2 k0 u3) in (drop
277 TMP_90 O TMP_92 TMP_93))))))) in (let TMP_95 \def (\lambda (e2: C).(\lambda
278 (_: T).(wcpr0 e2 e1))) in (let TMP_96 \def (\lambda (_: C).(\lambda (u3:
279 T).(pr0 u3 u0))) in (let TMP_97 \def (Bind b) in (let TMP_98 \def (CHead x0
280 k0 x1) in (let TMP_99 \def (drop_drop TMP_97 n c3 TMP_98 H6 u1) in
281 (ex3_2_intro C T TMP_94 TMP_95 TMP_96 x0 x1 TMP_99 H7 H8)))))))))))) in
282 (ex3_2_ind C T TMP_79 TMP_80 TMP_81 TMP_89 TMP_100 H5)))))))))))))))))))) in
283 (let TMP_130 \def (\lambda (f: F).(\lambda (n: nat).(\lambda (_: ((\forall
284 (e1: C).(\forall (u3: T).(\forall (k0: K).((drop n O (CHead c4 (Flat f) u2)
285 (CHead e1 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(drop n O
286 (CHead c3 (Flat f) u1) (CHead e2 k0 u4)))) (\lambda (e2: C).(\lambda (_:
287 T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u4: T).(pr0 u4
288 u3)))))))))).(\lambda (e1: C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H4:
289 (drop (S n) O (CHead c4 (Flat f) u2) (CHead e1 k0 u0))).(let TMP_102 \def (S
290 n) in (let TMP_103 \def (Flat f) in (let TMP_104 \def (CHead e1 k0 u0) in
291 (let TMP_105 \def (drop_gen_drop TMP_103 c4 TMP_104 u2 n H4) in (let H5 \def
292 (H1 TMP_102 e1 u0 k0 TMP_105) in (let TMP_108 \def (\lambda (e2: C).(\lambda
293 (u3: T).(let TMP_106 \def (S n) in (let TMP_107 \def (CHead e2 k0 u3) in
294 (drop TMP_106 O c3 TMP_107))))) in (let TMP_109 \def (\lambda (e2:
295 C).(\lambda (_: T).(wcpr0 e2 e1))) in (let TMP_110 \def (\lambda (_:
296 C).(\lambda (u3: T).(pr0 u3 u0))) in (let TMP_115 \def (\lambda (e2:
297 C).(\lambda (u3: T).(let TMP_111 \def (S n) in (let TMP_112 \def (Flat f) in
298 (let TMP_113 \def (CHead c3 TMP_112 u1) in (let TMP_114 \def (CHead e2 k0 u3)
299 in (drop TMP_111 O TMP_113 TMP_114))))))) in (let TMP_116 \def (\lambda (e2:
300 C).(\lambda (_: T).(wcpr0 e2 e1))) in (let TMP_117 \def (\lambda (_:
301 C).(\lambda (u3: T).(pr0 u3 u0))) in (let TMP_118 \def (ex3_2 C T TMP_115
302 TMP_116 TMP_117) in (let TMP_129 \def (\lambda (x0: C).(\lambda (x1:
303 T).(\lambda (H6: (drop (S n) O c3 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 x0
304 e1)).(\lambda (H8: (pr0 x1 u0)).(let TMP_123 \def (\lambda (e2: C).(\lambda
305 (u3: T).(let TMP_119 \def (S n) in (let TMP_120 \def (Flat f) in (let TMP_121
306 \def (CHead c3 TMP_120 u1) in (let TMP_122 \def (CHead e2 k0 u3) in (drop
307 TMP_119 O TMP_121 TMP_122))))))) in (let TMP_124 \def (\lambda (e2:
308 C).(\lambda (_: T).(wcpr0 e2 e1))) in (let TMP_125 \def (\lambda (_:
309 C).(\lambda (u3: T).(pr0 u3 u0))) in (let TMP_126 \def (Flat f) in (let
310 TMP_127 \def (CHead x0 k0 x1) in (let TMP_128 \def (drop_drop TMP_126 n c3
311 TMP_127 H6 u1) in (ex3_2_intro C T TMP_123 TMP_124 TMP_125 x0 x1 TMP_128 H7
312 H8)))))))))))) in (ex3_2_ind C T TMP_108 TMP_109 TMP_110 TMP_118 TMP_129
313 H5))))))))))))))))))))) in (let TMP_131 \def (K_ind TMP_74 TMP_101 TMP_130 k)
314 in (nat_ind TMP_18 TMP_67 TMP_131 h)))))))))))))))) in (wcpr0_ind TMP_5
315 TMP_12 TMP_132 c2 c1 H)))))).
318 \forall (c1: C).(\forall (c2: C).((wcpr0 c1 c2) \to (\forall (h:
319 nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((getl h c1 (CHead e1
320 k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(getl h c2 (CHead e2
321 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_:
322 C).(\lambda (u2: T).(pr0 u1 u2)))))))))))
324 \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (wcpr0 c1 c2)).(let TMP_5 \def
325 (\lambda (c: C).(\lambda (c0: C).(\forall (h: nat).(\forall (e1: C).(\forall
326 (u1: T).(\forall (k: K).((getl h c (CHead e1 k u1)) \to (let TMP_2 \def
327 (\lambda (e2: C).(\lambda (u2: T).(let TMP_1 \def (CHead e2 k u2) in (getl h
328 c0 TMP_1)))) in (let TMP_3 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1
329 e2))) in (let TMP_4 \def (\lambda (_: C).(\lambda (u2: T).(pr0 u1 u2))) in
330 (ex3_2 C T TMP_2 TMP_3 TMP_4))))))))))) in (let TMP_12 \def (\lambda (c:
331 C).(\lambda (h: nat).(\lambda (e1: C).(\lambda (u1: T).(\lambda (k:
332 K).(\lambda (H0: (getl h c (CHead e1 k u1))).(let TMP_7 \def (\lambda (e2:
333 C).(\lambda (u2: T).(let TMP_6 \def (CHead e2 k u2) in (getl h c TMP_6)))) in
334 (let TMP_8 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) in (let
335 TMP_9 \def (\lambda (_: C).(\lambda (u2: T).(pr0 u1 u2))) in (let TMP_10 \def
336 (wcpr0_refl e1) in (let TMP_11 \def (pr0_refl u1) in (ex3_2_intro C T TMP_7
337 TMP_8 TMP_9 e1 u1 H0 TMP_10 TMP_11)))))))))))) in (let TMP_175 \def (\lambda
338 (c3: C).(\lambda (c4: C).(\lambda (H0: (wcpr0 c3 c4)).(\lambda (H1: ((\forall
339 (h: nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((getl h c3 (CHead
340 e1 k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(getl h c4 (CHead
341 e2 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_:
342 C).(\lambda (u2: T).(pr0 u1 u2))))))))))).(\lambda (u1: T).(\lambda (u2:
343 T).(\lambda (H2: (pr0 u1 u2)).(\lambda (k: K).(\lambda (h: nat).(let TMP_18
344 \def (\lambda (n: nat).(\forall (e1: C).(\forall (u3: T).(\forall (k0:
345 K).((getl n (CHead c3 k u1) (CHead e1 k0 u3)) \to (let TMP_15 \def (\lambda
346 (e2: C).(\lambda (u4: T).(let TMP_13 \def (CHead c4 k u2) in (let TMP_14 \def
347 (CHead e2 k0 u4) in (getl n TMP_13 TMP_14))))) in (let TMP_16 \def (\lambda
348 (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) in (let TMP_17 \def (\lambda (_:
349 C).(\lambda (u4: T).(pr0 u3 u4))) in (ex3_2 C T TMP_15 TMP_16 TMP_17)))))))))
350 in (let TMP_110 \def (\lambda (e1: C).(\lambda (u0: T).(\lambda (k0:
351 K).(\lambda (H3: (getl O (CHead c3 k u1) (CHead e1 k0 u0))).(let TMP_24 \def
352 (\lambda (k1: K).((clear (CHead c3 k1 u1) (CHead e1 k0 u0)) \to (let TMP_21
353 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_19 \def (CHead c4 k1 u2) in
354 (let TMP_20 \def (CHead e2 k0 u3) in (getl O TMP_19 TMP_20))))) in (let
355 TMP_22 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) in (let TMP_23
356 \def (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))) in (ex3_2 C T TMP_21
357 TMP_22 TMP_23)))))) in (let TMP_80 \def (\lambda (b: B).(\lambda (H4: (clear
358 (CHead c3 (Bind b) u1) (CHead e1 k0 u0))).(let TMP_25 \def (\lambda (e:
359 C).(match e with [(CSort _) \Rightarrow e1 | (CHead c _ _) \Rightarrow c]))
360 in (let TMP_26 \def (CHead e1 k0 u0) in (let TMP_27 \def (Bind b) in (let
361 TMP_28 \def (CHead c3 TMP_27 u1) in (let TMP_29 \def (CHead e1 k0 u0) in (let
362 TMP_30 \def (clear_gen_bind b c3 TMP_29 u1 H4) in (let H5 \def (f_equal C C
363 TMP_25 TMP_26 TMP_28 TMP_30) in (let TMP_31 \def (\lambda (e: C).(match e
364 with [(CSort _) \Rightarrow k0 | (CHead _ k1 _) \Rightarrow k1])) in (let
365 TMP_32 \def (CHead e1 k0 u0) in (let TMP_33 \def (Bind b) in (let TMP_34 \def
366 (CHead c3 TMP_33 u1) in (let TMP_35 \def (CHead e1 k0 u0) in (let TMP_36 \def
367 (clear_gen_bind b c3 TMP_35 u1 H4) in (let H6 \def (f_equal C K TMP_31 TMP_32
368 TMP_34 TMP_36) in (let TMP_37 \def (\lambda (e: C).(match e with [(CSort _)
369 \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) in (let TMP_38 \def (CHead e1
370 k0 u0) in (let TMP_39 \def (Bind b) in (let TMP_40 \def (CHead c3 TMP_39 u1)
371 in (let TMP_41 \def (CHead e1 k0 u0) in (let TMP_42 \def (clear_gen_bind b c3
372 TMP_41 u1 H4) in (let H7 \def (f_equal C T TMP_37 TMP_38 TMP_40 TMP_42) in
373 (let TMP_78 \def (\lambda (H8: (eq K k0 (Bind b))).(\lambda (H9: (eq C e1
374 c3)).(let TMP_43 \def (Bind b) in (let TMP_50 \def (\lambda (k1: K).(let
375 TMP_47 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_44 \def (Bind b) in
376 (let TMP_45 \def (CHead c4 TMP_44 u2) in (let TMP_46 \def (CHead e2 k1 u3) in
377 (getl O TMP_45 TMP_46)))))) in (let TMP_48 \def (\lambda (e2: C).(\lambda (_:
378 T).(wcpr0 e1 e2))) in (let TMP_49 \def (\lambda (_: C).(\lambda (u3: T).(pr0
379 u0 u3))) in (ex3_2 C T TMP_47 TMP_48 TMP_49))))) in (let TMP_58 \def (\lambda
380 (t: T).(let TMP_55 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_51 \def
381 (Bind b) in (let TMP_52 \def (CHead c4 TMP_51 u2) in (let TMP_53 \def (Bind
382 b) in (let TMP_54 \def (CHead e2 TMP_53 u3) in (getl O TMP_52 TMP_54)))))))
383 in (let TMP_56 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) in (let
384 TMP_57 \def (\lambda (_: C).(\lambda (u3: T).(pr0 t u3))) in (ex3_2 C T
385 TMP_55 TMP_56 TMP_57))))) in (let TMP_66 \def (\lambda (c: C).(let TMP_63
386 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_59 \def (Bind b) in (let
387 TMP_60 \def (CHead c4 TMP_59 u2) in (let TMP_61 \def (Bind b) in (let TMP_62
388 \def (CHead e2 TMP_61 u3) in (getl O TMP_60 TMP_62))))))) in (let TMP_64 \def
389 (\lambda (e2: C).(\lambda (_: T).(wcpr0 c e2))) in (let TMP_65 \def (\lambda
390 (_: C).(\lambda (u3: T).(pr0 u1 u3))) in (ex3_2 C T TMP_63 TMP_64 TMP_65)))))
391 in (let TMP_71 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_67 \def (Bind
392 b) in (let TMP_68 \def (CHead c4 TMP_67 u2) in (let TMP_69 \def (Bind b) in
393 (let TMP_70 \def (CHead e2 TMP_69 u3) in (getl O TMP_68 TMP_70))))))) in (let
394 TMP_72 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 c3 e2))) in (let TMP_73
395 \def (\lambda (_: C).(\lambda (u3: T).(pr0 u1 u3))) in (let TMP_74 \def
396 (getl_refl b c4 u2) in (let TMP_75 \def (ex3_2_intro C T TMP_71 TMP_72 TMP_73
397 c4 u2 TMP_74 H0 H2) in (let TMP_76 \def (eq_ind_r C c3 TMP_66 TMP_75 e1 H9)
398 in (let TMP_77 \def (eq_ind_r T u1 TMP_58 TMP_76 u0 H7) in (eq_ind_r K TMP_43
399 TMP_50 TMP_77 k0 H8)))))))))))))) in (let TMP_79 \def (TMP_78 H6) in (TMP_79
400 H5)))))))))))))))))))))))))) in (let TMP_106 \def (\lambda (f: F).(\lambda
401 (H4: (clear (CHead c3 (Flat f) u1) (CHead e1 k0 u0))).(let TMP_81 \def (CHead
402 e1 k0 u0) in (let TMP_82 \def (drop_refl c3) in (let TMP_83 \def (CHead e1 k0
403 u0) in (let TMP_84 \def (clear_gen_flat f c3 TMP_83 u1 H4) in (let TMP_85
404 \def (getl_intro O c3 TMP_81 c3 TMP_82 TMP_84) in (let H5 \def (H1 O e1 u0 k0
405 TMP_85) in (let TMP_87 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_86
406 \def (CHead e2 k0 u3) in (getl O c4 TMP_86)))) in (let TMP_88 \def (\lambda
407 (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) in (let TMP_89 \def (\lambda (_:
408 C).(\lambda (u3: T).(pr0 u0 u3))) in (let TMP_93 \def (\lambda (e2:
409 C).(\lambda (u3: T).(let TMP_90 \def (Flat f) in (let TMP_91 \def (CHead c4
410 TMP_90 u2) in (let TMP_92 \def (CHead e2 k0 u3) in (getl O TMP_91
411 TMP_92)))))) in (let TMP_94 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1
412 e2))) in (let TMP_95 \def (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))) in
413 (let TMP_96 \def (ex3_2 C T TMP_93 TMP_94 TMP_95) in (let TMP_105 \def
414 (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (getl O c4 (CHead x0 k0
415 x1))).(\lambda (H7: (wcpr0 e1 x0)).(\lambda (H8: (pr0 u0 x1)).(let TMP_100
416 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_97 \def (Flat f) in (let
417 TMP_98 \def (CHead c4 TMP_97 u2) in (let TMP_99 \def (CHead e2 k0 u3) in
418 (getl O TMP_98 TMP_99)))))) in (let TMP_101 \def (\lambda (e2: C).(\lambda
419 (_: T).(wcpr0 e1 e2))) in (let TMP_102 \def (\lambda (_: C).(\lambda (u3:
420 T).(pr0 u0 u3))) in (let TMP_103 \def (CHead x0 k0 x1) in (let TMP_104 \def
421 (getl_flat c4 TMP_103 O H6 f u2) in (ex3_2_intro C T TMP_100 TMP_101 TMP_102
422 x0 x1 TMP_104 H7 H8))))))))))) in (ex3_2_ind C T TMP_87 TMP_88 TMP_89 TMP_96
423 TMP_105 H5))))))))))))))))) in (let TMP_107 \def (CHead c3 k u1) in (let
424 TMP_108 \def (CHead e1 k0 u0) in (let TMP_109 \def (getl_gen_O TMP_107
425 TMP_108 H3) in (K_ind TMP_24 TMP_80 TMP_106 k TMP_109))))))))))) in (let
426 TMP_117 \def (\lambda (k0: K).(\forall (n: nat).(((\forall (e1: C).(\forall
427 (u3: T).(\forall (k1: K).((getl n (CHead c3 k0 u1) (CHead e1 k1 u3)) \to
428 (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(getl n (CHead c4 k0 u2) (CHead
429 e2 k1 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_:
430 C).(\lambda (u4: T).(pr0 u3 u4))))))))) \to (\forall (e1: C).(\forall (u3:
431 T).(\forall (k1: K).((getl (S n) (CHead c3 k0 u1) (CHead e1 k1 u3)) \to (let
432 TMP_114 \def (\lambda (e2: C).(\lambda (u4: T).(let TMP_111 \def (S n) in
433 (let TMP_112 \def (CHead c4 k0 u2) in (let TMP_113 \def (CHead e2 k1 u4) in
434 (getl TMP_111 TMP_112 TMP_113)))))) in (let TMP_115 \def (\lambda (e2:
435 C).(\lambda (_: T).(wcpr0 e1 e2))) in (let TMP_116 \def (\lambda (_:
436 C).(\lambda (u4: T).(pr0 u3 u4))) in (ex3_2 C T TMP_114 TMP_115
437 TMP_116))))))))))) in (let TMP_144 \def (\lambda (b: B).(\lambda (n:
438 nat).(\lambda (_: ((\forall (e1: C).(\forall (u3: T).(\forall (k0: K).((getl
439 n (CHead c3 (Bind b) u1) (CHead e1 k0 u3)) \to (ex3_2 C T (\lambda (e2:
440 C).(\lambda (u4: T).(getl n (CHead c4 (Bind b) u2) (CHead e2 k0 u4))))
441 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda
442 (u4: T).(pr0 u3 u4)))))))))).(\lambda (e1: C).(\lambda (u0: T).(\lambda (k0:
443 K).(\lambda (H4: (getl (S n) (CHead c3 (Bind b) u1) (CHead e1 k0 u0))).(let
444 TMP_118 \def (Bind b) in (let TMP_119 \def (CHead e1 k0 u0) in (let TMP_120
445 \def (getl_gen_S TMP_118 c3 TMP_119 u1 n H4) in (let H5 \def (H1 n e1 u0 k0
446 TMP_120) in (let TMP_122 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_121
447 \def (CHead e2 k0 u3) in (getl n c4 TMP_121)))) in (let TMP_123 \def (\lambda
448 (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) in (let TMP_124 \def (\lambda (_:
449 C).(\lambda (u3: T).(pr0 u0 u3))) in (let TMP_129 \def (\lambda (e2:
450 C).(\lambda (u3: T).(let TMP_125 \def (S n) in (let TMP_126 \def (Bind b) in
451 (let TMP_127 \def (CHead c4 TMP_126 u2) in (let TMP_128 \def (CHead e2 k0 u3)
452 in (getl TMP_125 TMP_127 TMP_128))))))) in (let TMP_130 \def (\lambda (e2:
453 C).(\lambda (_: T).(wcpr0 e1 e2))) in (let TMP_131 \def (\lambda (_:
454 C).(\lambda (u3: T).(pr0 u0 u3))) in (let TMP_132 \def (ex3_2 C T TMP_129
455 TMP_130 TMP_131) in (let TMP_143 \def (\lambda (x0: C).(\lambda (x1:
456 T).(\lambda (H6: (getl n c4 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 e1
457 x0)).(\lambda (H8: (pr0 u0 x1)).(let TMP_137 \def (\lambda (e2: C).(\lambda
458 (u3: T).(let TMP_133 \def (S n) in (let TMP_134 \def (Bind b) in (let TMP_135
459 \def (CHead c4 TMP_134 u2) in (let TMP_136 \def (CHead e2 k0 u3) in (getl
460 TMP_133 TMP_135 TMP_136))))))) in (let TMP_138 \def (\lambda (e2: C).(\lambda
461 (_: T).(wcpr0 e1 e2))) in (let TMP_139 \def (\lambda (_: C).(\lambda (u3:
462 T).(pr0 u0 u3))) in (let TMP_140 \def (Bind b) in (let TMP_141 \def (CHead x0
463 k0 x1) in (let TMP_142 \def (getl_head TMP_140 n c4 TMP_141 H6 u2) in
464 (ex3_2_intro C T TMP_137 TMP_138 TMP_139 x0 x1 TMP_142 H7 H8)))))))))))) in
465 (ex3_2_ind C T TMP_122 TMP_123 TMP_124 TMP_132 TMP_143 H5))))))))))))))))))))
466 in (let TMP_173 \def (\lambda (f: F).(\lambda (n: nat).(\lambda (_: ((\forall
467 (e1: C).(\forall (u3: T).(\forall (k0: K).((getl n (CHead c3 (Flat f) u1)
468 (CHead e1 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(getl n
469 (CHead c4 (Flat f) u2) (CHead e2 k0 u4)))) (\lambda (e2: C).(\lambda (_:
470 T).(wcpr0 e1 e2))) (\lambda (_: C).(\lambda (u4: T).(pr0 u3
471 u4)))))))))).(\lambda (e1: C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H4:
472 (getl (S n) (CHead c3 (Flat f) u1) (CHead e1 k0 u0))).(let TMP_145 \def (S n)
473 in (let TMP_146 \def (Flat f) in (let TMP_147 \def (CHead e1 k0 u0) in (let
474 TMP_148 \def (getl_gen_S TMP_146 c3 TMP_147 u1 n H4) in (let H5 \def (H1
475 TMP_145 e1 u0 k0 TMP_148) in (let TMP_151 \def (\lambda (e2: C).(\lambda (u3:
476 T).(let TMP_149 \def (S n) in (let TMP_150 \def (CHead e2 k0 u3) in (getl
477 TMP_149 c4 TMP_150))))) in (let TMP_152 \def (\lambda (e2: C).(\lambda (_:
478 T).(wcpr0 e1 e2))) in (let TMP_153 \def (\lambda (_: C).(\lambda (u3: T).(pr0
479 u0 u3))) in (let TMP_158 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_154
480 \def (S n) in (let TMP_155 \def (Flat f) in (let TMP_156 \def (CHead c4
481 TMP_155 u2) in (let TMP_157 \def (CHead e2 k0 u3) in (getl TMP_154 TMP_156
482 TMP_157))))))) in (let TMP_159 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0
483 e1 e2))) in (let TMP_160 \def (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3)))
484 in (let TMP_161 \def (ex3_2 C T TMP_158 TMP_159 TMP_160) in (let TMP_172 \def
485 (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (getl (S n) c4 (CHead x0 k0
486 x1))).(\lambda (H7: (wcpr0 e1 x0)).(\lambda (H8: (pr0 u0 x1)).(let TMP_166
487 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_162 \def (S n) in (let
488 TMP_163 \def (Flat f) in (let TMP_164 \def (CHead c4 TMP_163 u2) in (let
489 TMP_165 \def (CHead e2 k0 u3) in (getl TMP_162 TMP_164 TMP_165))))))) in (let
490 TMP_167 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e1 e2))) in (let TMP_168
491 \def (\lambda (_: C).(\lambda (u3: T).(pr0 u0 u3))) in (let TMP_169 \def
492 (Flat f) in (let TMP_170 \def (CHead x0 k0 x1) in (let TMP_171 \def
493 (getl_head TMP_169 n c4 TMP_170 H6 u2) in (ex3_2_intro C T TMP_166 TMP_167
494 TMP_168 x0 x1 TMP_171 H7 H8)))))))))))) in (ex3_2_ind C T TMP_151 TMP_152
495 TMP_153 TMP_161 TMP_172 H5))))))))))))))))))))) in (let TMP_174 \def (K_ind
496 TMP_117 TMP_144 TMP_173 k) in (nat_ind TMP_18 TMP_110 TMP_174
497 h)))))))))))))))) in (wcpr0_ind TMP_5 TMP_12 TMP_175 c1 c2 H)))))).
499 theorem wcpr0_getl_back:
500 \forall (c1: C).(\forall (c2: C).((wcpr0 c2 c1) \to (\forall (h:
501 nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((getl h c1 (CHead e1
502 k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(getl h c2 (CHead e2
503 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_:
504 C).(\lambda (u2: T).(pr0 u2 u1)))))))))))
506 \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (wcpr0 c2 c1)).(let TMP_5 \def
507 (\lambda (c: C).(\lambda (c0: C).(\forall (h: nat).(\forall (e1: C).(\forall
508 (u1: T).(\forall (k: K).((getl h c0 (CHead e1 k u1)) \to (let TMP_2 \def
509 (\lambda (e2: C).(\lambda (u2: T).(let TMP_1 \def (CHead e2 k u2) in (getl h
510 c TMP_1)))) in (let TMP_3 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2
511 e1))) in (let TMP_4 \def (\lambda (_: C).(\lambda (u2: T).(pr0 u2 u1))) in
512 (ex3_2 C T TMP_2 TMP_3 TMP_4))))))))))) in (let TMP_12 \def (\lambda (c:
513 C).(\lambda (h: nat).(\lambda (e1: C).(\lambda (u1: T).(\lambda (k:
514 K).(\lambda (H0: (getl h c (CHead e1 k u1))).(let TMP_7 \def (\lambda (e2:
515 C).(\lambda (u2: T).(let TMP_6 \def (CHead e2 k u2) in (getl h c TMP_6)))) in
516 (let TMP_8 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) in (let
517 TMP_9 \def (\lambda (_: C).(\lambda (u2: T).(pr0 u2 u1))) in (let TMP_10 \def
518 (wcpr0_refl e1) in (let TMP_11 \def (pr0_refl u1) in (ex3_2_intro C T TMP_7
519 TMP_8 TMP_9 e1 u1 H0 TMP_10 TMP_11)))))))))))) in (let TMP_175 \def (\lambda
520 (c3: C).(\lambda (c4: C).(\lambda (H0: (wcpr0 c3 c4)).(\lambda (H1: ((\forall
521 (h: nat).(\forall (e1: C).(\forall (u1: T).(\forall (k: K).((getl h c4 (CHead
522 e1 k u1)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u2: T).(getl h c3 (CHead
523 e2 k u2)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_:
524 C).(\lambda (u2: T).(pr0 u2 u1))))))))))).(\lambda (u1: T).(\lambda (u2:
525 T).(\lambda (H2: (pr0 u1 u2)).(\lambda (k: K).(\lambda (h: nat).(let TMP_18
526 \def (\lambda (n: nat).(\forall (e1: C).(\forall (u3: T).(\forall (k0:
527 K).((getl n (CHead c4 k u2) (CHead e1 k0 u3)) \to (let TMP_15 \def (\lambda
528 (e2: C).(\lambda (u4: T).(let TMP_13 \def (CHead c3 k u1) in (let TMP_14 \def
529 (CHead e2 k0 u4) in (getl n TMP_13 TMP_14))))) in (let TMP_16 \def (\lambda
530 (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) in (let TMP_17 \def (\lambda (_:
531 C).(\lambda (u4: T).(pr0 u4 u3))) in (ex3_2 C T TMP_15 TMP_16 TMP_17)))))))))
532 in (let TMP_110 \def (\lambda (e1: C).(\lambda (u0: T).(\lambda (k0:
533 K).(\lambda (H3: (getl O (CHead c4 k u2) (CHead e1 k0 u0))).(let TMP_24 \def
534 (\lambda (k1: K).((clear (CHead c4 k1 u2) (CHead e1 k0 u0)) \to (let TMP_21
535 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_19 \def (CHead c3 k1 u1) in
536 (let TMP_20 \def (CHead e2 k0 u3) in (getl O TMP_19 TMP_20))))) in (let
537 TMP_22 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) in (let TMP_23
538 \def (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))) in (ex3_2 C T TMP_21
539 TMP_22 TMP_23)))))) in (let TMP_80 \def (\lambda (b: B).(\lambda (H4: (clear
540 (CHead c4 (Bind b) u2) (CHead e1 k0 u0))).(let TMP_25 \def (\lambda (e:
541 C).(match e with [(CSort _) \Rightarrow e1 | (CHead c _ _) \Rightarrow c]))
542 in (let TMP_26 \def (CHead e1 k0 u0) in (let TMP_27 \def (Bind b) in (let
543 TMP_28 \def (CHead c4 TMP_27 u2) in (let TMP_29 \def (CHead e1 k0 u0) in (let
544 TMP_30 \def (clear_gen_bind b c4 TMP_29 u2 H4) in (let H5 \def (f_equal C C
545 TMP_25 TMP_26 TMP_28 TMP_30) in (let TMP_31 \def (\lambda (e: C).(match e
546 with [(CSort _) \Rightarrow k0 | (CHead _ k1 _) \Rightarrow k1])) in (let
547 TMP_32 \def (CHead e1 k0 u0) in (let TMP_33 \def (Bind b) in (let TMP_34 \def
548 (CHead c4 TMP_33 u2) in (let TMP_35 \def (CHead e1 k0 u0) in (let TMP_36 \def
549 (clear_gen_bind b c4 TMP_35 u2 H4) in (let H6 \def (f_equal C K TMP_31 TMP_32
550 TMP_34 TMP_36) in (let TMP_37 \def (\lambda (e: C).(match e with [(CSort _)
551 \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) in (let TMP_38 \def (CHead e1
552 k0 u0) in (let TMP_39 \def (Bind b) in (let TMP_40 \def (CHead c4 TMP_39 u2)
553 in (let TMP_41 \def (CHead e1 k0 u0) in (let TMP_42 \def (clear_gen_bind b c4
554 TMP_41 u2 H4) in (let H7 \def (f_equal C T TMP_37 TMP_38 TMP_40 TMP_42) in
555 (let TMP_78 \def (\lambda (H8: (eq K k0 (Bind b))).(\lambda (H9: (eq C e1
556 c4)).(let TMP_43 \def (Bind b) in (let TMP_50 \def (\lambda (k1: K).(let
557 TMP_47 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_44 \def (Bind b) in
558 (let TMP_45 \def (CHead c3 TMP_44 u1) in (let TMP_46 \def (CHead e2 k1 u3) in
559 (getl O TMP_45 TMP_46)))))) in (let TMP_48 \def (\lambda (e2: C).(\lambda (_:
560 T).(wcpr0 e2 e1))) in (let TMP_49 \def (\lambda (_: C).(\lambda (u3: T).(pr0
561 u3 u0))) in (ex3_2 C T TMP_47 TMP_48 TMP_49))))) in (let TMP_58 \def (\lambda
562 (t: T).(let TMP_55 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_51 \def
563 (Bind b) in (let TMP_52 \def (CHead c3 TMP_51 u1) in (let TMP_53 \def (Bind
564 b) in (let TMP_54 \def (CHead e2 TMP_53 u3) in (getl O TMP_52 TMP_54)))))))
565 in (let TMP_56 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) in (let
566 TMP_57 \def (\lambda (_: C).(\lambda (u3: T).(pr0 u3 t))) in (ex3_2 C T
567 TMP_55 TMP_56 TMP_57))))) in (let TMP_66 \def (\lambda (c: C).(let TMP_63
568 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_59 \def (Bind b) in (let
569 TMP_60 \def (CHead c3 TMP_59 u1) in (let TMP_61 \def (Bind b) in (let TMP_62
570 \def (CHead e2 TMP_61 u3) in (getl O TMP_60 TMP_62))))))) in (let TMP_64 \def
571 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 c))) in (let TMP_65 \def (\lambda
572 (_: C).(\lambda (u3: T).(pr0 u3 u2))) in (ex3_2 C T TMP_63 TMP_64 TMP_65)))))
573 in (let TMP_71 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_67 \def (Bind
574 b) in (let TMP_68 \def (CHead c3 TMP_67 u1) in (let TMP_69 \def (Bind b) in
575 (let TMP_70 \def (CHead e2 TMP_69 u3) in (getl O TMP_68 TMP_70))))))) in (let
576 TMP_72 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 c4))) in (let TMP_73
577 \def (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u2))) in (let TMP_74 \def
578 (getl_refl b c3 u1) in (let TMP_75 \def (ex3_2_intro C T TMP_71 TMP_72 TMP_73
579 c3 u1 TMP_74 H0 H2) in (let TMP_76 \def (eq_ind_r C c4 TMP_66 TMP_75 e1 H9)
580 in (let TMP_77 \def (eq_ind_r T u2 TMP_58 TMP_76 u0 H7) in (eq_ind_r K TMP_43
581 TMP_50 TMP_77 k0 H8)))))))))))))) in (let TMP_79 \def (TMP_78 H6) in (TMP_79
582 H5)))))))))))))))))))))))))) in (let TMP_106 \def (\lambda (f: F).(\lambda
583 (H4: (clear (CHead c4 (Flat f) u2) (CHead e1 k0 u0))).(let TMP_81 \def (CHead
584 e1 k0 u0) in (let TMP_82 \def (drop_refl c4) in (let TMP_83 \def (CHead e1 k0
585 u0) in (let TMP_84 \def (clear_gen_flat f c4 TMP_83 u2 H4) in (let TMP_85
586 \def (getl_intro O c4 TMP_81 c4 TMP_82 TMP_84) in (let H5 \def (H1 O e1 u0 k0
587 TMP_85) in (let TMP_87 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_86
588 \def (CHead e2 k0 u3) in (getl O c3 TMP_86)))) in (let TMP_88 \def (\lambda
589 (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) in (let TMP_89 \def (\lambda (_:
590 C).(\lambda (u3: T).(pr0 u3 u0))) in (let TMP_93 \def (\lambda (e2:
591 C).(\lambda (u3: T).(let TMP_90 \def (Flat f) in (let TMP_91 \def (CHead c3
592 TMP_90 u1) in (let TMP_92 \def (CHead e2 k0 u3) in (getl O TMP_91
593 TMP_92)))))) in (let TMP_94 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2
594 e1))) in (let TMP_95 \def (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))) in
595 (let TMP_96 \def (ex3_2 C T TMP_93 TMP_94 TMP_95) in (let TMP_105 \def
596 (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (getl O c3 (CHead x0 k0
597 x1))).(\lambda (H7: (wcpr0 x0 e1)).(\lambda (H8: (pr0 x1 u0)).(let TMP_100
598 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_97 \def (Flat f) in (let
599 TMP_98 \def (CHead c3 TMP_97 u1) in (let TMP_99 \def (CHead e2 k0 u3) in
600 (getl O TMP_98 TMP_99)))))) in (let TMP_101 \def (\lambda (e2: C).(\lambda
601 (_: T).(wcpr0 e2 e1))) in (let TMP_102 \def (\lambda (_: C).(\lambda (u3:
602 T).(pr0 u3 u0))) in (let TMP_103 \def (CHead x0 k0 x1) in (let TMP_104 \def
603 (getl_flat c3 TMP_103 O H6 f u1) in (ex3_2_intro C T TMP_100 TMP_101 TMP_102
604 x0 x1 TMP_104 H7 H8))))))))))) in (ex3_2_ind C T TMP_87 TMP_88 TMP_89 TMP_96
605 TMP_105 H5))))))))))))))))) in (let TMP_107 \def (CHead c4 k u2) in (let
606 TMP_108 \def (CHead e1 k0 u0) in (let TMP_109 \def (getl_gen_O TMP_107
607 TMP_108 H3) in (K_ind TMP_24 TMP_80 TMP_106 k TMP_109))))))))))) in (let
608 TMP_117 \def (\lambda (k0: K).(\forall (n: nat).(((\forall (e1: C).(\forall
609 (u3: T).(\forall (k1: K).((getl n (CHead c4 k0 u2) (CHead e1 k1 u3)) \to
610 (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(getl n (CHead c3 k0 u1) (CHead
611 e2 k1 u4)))) (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_:
612 C).(\lambda (u4: T).(pr0 u4 u3))))))))) \to (\forall (e1: C).(\forall (u3:
613 T).(\forall (k1: K).((getl (S n) (CHead c4 k0 u2) (CHead e1 k1 u3)) \to (let
614 TMP_114 \def (\lambda (e2: C).(\lambda (u4: T).(let TMP_111 \def (S n) in
615 (let TMP_112 \def (CHead c3 k0 u1) in (let TMP_113 \def (CHead e2 k1 u4) in
616 (getl TMP_111 TMP_112 TMP_113)))))) in (let TMP_115 \def (\lambda (e2:
617 C).(\lambda (_: T).(wcpr0 e2 e1))) in (let TMP_116 \def (\lambda (_:
618 C).(\lambda (u4: T).(pr0 u4 u3))) in (ex3_2 C T TMP_114 TMP_115
619 TMP_116))))))))))) in (let TMP_144 \def (\lambda (b: B).(\lambda (n:
620 nat).(\lambda (_: ((\forall (e1: C).(\forall (u3: T).(\forall (k0: K).((getl
621 n (CHead c4 (Bind b) u2) (CHead e1 k0 u3)) \to (ex3_2 C T (\lambda (e2:
622 C).(\lambda (u4: T).(getl n (CHead c3 (Bind b) u1) (CHead e2 k0 u4))))
623 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda
624 (u4: T).(pr0 u4 u3)))))))))).(\lambda (e1: C).(\lambda (u0: T).(\lambda (k0:
625 K).(\lambda (H4: (getl (S n) (CHead c4 (Bind b) u2) (CHead e1 k0 u0))).(let
626 TMP_118 \def (Bind b) in (let TMP_119 \def (CHead e1 k0 u0) in (let TMP_120
627 \def (getl_gen_S TMP_118 c4 TMP_119 u2 n H4) in (let H5 \def (H1 n e1 u0 k0
628 TMP_120) in (let TMP_122 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_121
629 \def (CHead e2 k0 u3) in (getl n c3 TMP_121)))) in (let TMP_123 \def (\lambda
630 (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) in (let TMP_124 \def (\lambda (_:
631 C).(\lambda (u3: T).(pr0 u3 u0))) in (let TMP_129 \def (\lambda (e2:
632 C).(\lambda (u3: T).(let TMP_125 \def (S n) in (let TMP_126 \def (Bind b) in
633 (let TMP_127 \def (CHead c3 TMP_126 u1) in (let TMP_128 \def (CHead e2 k0 u3)
634 in (getl TMP_125 TMP_127 TMP_128))))))) in (let TMP_130 \def (\lambda (e2:
635 C).(\lambda (_: T).(wcpr0 e2 e1))) in (let TMP_131 \def (\lambda (_:
636 C).(\lambda (u3: T).(pr0 u3 u0))) in (let TMP_132 \def (ex3_2 C T TMP_129
637 TMP_130 TMP_131) in (let TMP_143 \def (\lambda (x0: C).(\lambda (x1:
638 T).(\lambda (H6: (getl n c3 (CHead x0 k0 x1))).(\lambda (H7: (wcpr0 x0
639 e1)).(\lambda (H8: (pr0 x1 u0)).(let TMP_137 \def (\lambda (e2: C).(\lambda
640 (u3: T).(let TMP_133 \def (S n) in (let TMP_134 \def (Bind b) in (let TMP_135
641 \def (CHead c3 TMP_134 u1) in (let TMP_136 \def (CHead e2 k0 u3) in (getl
642 TMP_133 TMP_135 TMP_136))))))) in (let TMP_138 \def (\lambda (e2: C).(\lambda
643 (_: T).(wcpr0 e2 e1))) in (let TMP_139 \def (\lambda (_: C).(\lambda (u3:
644 T).(pr0 u3 u0))) in (let TMP_140 \def (Bind b) in (let TMP_141 \def (CHead x0
645 k0 x1) in (let TMP_142 \def (getl_head TMP_140 n c3 TMP_141 H6 u1) in
646 (ex3_2_intro C T TMP_137 TMP_138 TMP_139 x0 x1 TMP_142 H7 H8)))))))))))) in
647 (ex3_2_ind C T TMP_122 TMP_123 TMP_124 TMP_132 TMP_143 H5))))))))))))))))))))
648 in (let TMP_173 \def (\lambda (f: F).(\lambda (n: nat).(\lambda (_: ((\forall
649 (e1: C).(\forall (u3: T).(\forall (k0: K).((getl n (CHead c4 (Flat f) u2)
650 (CHead e1 k0 u3)) \to (ex3_2 C T (\lambda (e2: C).(\lambda (u4: T).(getl n
651 (CHead c3 (Flat f) u1) (CHead e2 k0 u4)))) (\lambda (e2: C).(\lambda (_:
652 T).(wcpr0 e2 e1))) (\lambda (_: C).(\lambda (u4: T).(pr0 u4
653 u3)))))))))).(\lambda (e1: C).(\lambda (u0: T).(\lambda (k0: K).(\lambda (H4:
654 (getl (S n) (CHead c4 (Flat f) u2) (CHead e1 k0 u0))).(let TMP_145 \def (S n)
655 in (let TMP_146 \def (Flat f) in (let TMP_147 \def (CHead e1 k0 u0) in (let
656 TMP_148 \def (getl_gen_S TMP_146 c4 TMP_147 u2 n H4) in (let H5 \def (H1
657 TMP_145 e1 u0 k0 TMP_148) in (let TMP_151 \def (\lambda (e2: C).(\lambda (u3:
658 T).(let TMP_149 \def (S n) in (let TMP_150 \def (CHead e2 k0 u3) in (getl
659 TMP_149 c3 TMP_150))))) in (let TMP_152 \def (\lambda (e2: C).(\lambda (_:
660 T).(wcpr0 e2 e1))) in (let TMP_153 \def (\lambda (_: C).(\lambda (u3: T).(pr0
661 u3 u0))) in (let TMP_158 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_154
662 \def (S n) in (let TMP_155 \def (Flat f) in (let TMP_156 \def (CHead c3
663 TMP_155 u1) in (let TMP_157 \def (CHead e2 k0 u3) in (getl TMP_154 TMP_156
664 TMP_157))))))) in (let TMP_159 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0
665 e2 e1))) in (let TMP_160 \def (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0)))
666 in (let TMP_161 \def (ex3_2 C T TMP_158 TMP_159 TMP_160) in (let TMP_172 \def
667 (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (getl (S n) c3 (CHead x0 k0
668 x1))).(\lambda (H7: (wcpr0 x0 e1)).(\lambda (H8: (pr0 x1 u0)).(let TMP_166
669 \def (\lambda (e2: C).(\lambda (u3: T).(let TMP_162 \def (S n) in (let
670 TMP_163 \def (Flat f) in (let TMP_164 \def (CHead c3 TMP_163 u1) in (let
671 TMP_165 \def (CHead e2 k0 u3) in (getl TMP_162 TMP_164 TMP_165))))))) in (let
672 TMP_167 \def (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 e1))) in (let TMP_168
673 \def (\lambda (_: C).(\lambda (u3: T).(pr0 u3 u0))) in (let TMP_169 \def
674 (Flat f) in (let TMP_170 \def (CHead x0 k0 x1) in (let TMP_171 \def
675 (getl_head TMP_169 n c3 TMP_170 H6 u1) in (ex3_2_intro C T TMP_166 TMP_167
676 TMP_168 x0 x1 TMP_171 H7 H8)))))))))))) in (ex3_2_ind C T TMP_151 TMP_152
677 TMP_153 TMP_161 TMP_172 H5))))))))))))))))))))) in (let TMP_174 \def (K_ind
678 TMP_117 TMP_144 TMP_173 k) in (nat_ind TMP_18 TMP_110 TMP_174
679 h)))))))))))))))) in (wcpr0_ind TMP_5 TMP_12 TMP_175 c2 c1 H)))))).
projects / helm.git / blob