-(_: T).(drop h0 (r k d) c e0)))))))).(\lambda (u0: T).(\lambda (H4: (eq nat
-(S d0) (S d))).(\lambda (H5: (eq C (CHead c0 k0 (lift h0 (r k0 d0) u0))
-(CHead c k u))).(let TMP_100 \def (\lambda (e0: C).(match e0 with [(CSort _)
-\Rightarrow c0 | (CHead c1 _ _) \Rightarrow c1])) in (let TMP_101 \def (r k0
-d0) in (let TMP_102 \def (lift h0 TMP_101 u0) in (let TMP_103 \def (CHead c0
-k0 TMP_102) in (let TMP_104 \def (CHead c k u) in (let H6 \def (f_equal C C
-TMP_100 TMP_103 TMP_104 H5) in (let TMP_105 \def (\lambda (e0: C).(match e0
-with [(CSort _) \Rightarrow k0 | (CHead _ k1 _) \Rightarrow k1])) in (let
-TMP_106 \def (r k0 d0) in (let TMP_107 \def (lift h0 TMP_106 u0) in (let
-TMP_108 \def (CHead c0 k0 TMP_107) in (let TMP_109 \def (CHead c k u) in (let
-H7 \def (f_equal C K TMP_105 TMP_108 TMP_109 H5) in (let TMP_117 \def
-(\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow (let TMP_115 \def
-(\lambda (x0: nat).(plus x0 h0)) in (let TMP_116 \def (r k0 d0) in (lref_map
-TMP_115 TMP_116 u0))) | (CHead _ _ t) \Rightarrow t])) in (let TMP_118 \def
-(r k0 d0) in (let TMP_119 \def (lift h0 TMP_118 u0) in (let TMP_120 \def
-(CHead c0 k0 TMP_119) in (let TMP_121 \def (CHead c k u) in (let H8 \def
-(f_equal C T TMP_117 TMP_120 TMP_121 H5) in (let TMP_219 \def (\lambda (H9:
-(eq K k0 k)).(\lambda (H10: (eq C c0 c)).(let TMP_129 \def (\lambda (c1:
-C).((eq nat (r k0 d0) (S d)) \to ((eq C c1 (CHead c k u)) \to (let TMP_123
-\def (\lambda (e0: C).(\lambda (v: T).(let TMP_122 \def (CHead e0 k v) in (eq
-C e TMP_122)))) in (let TMP_126 \def (\lambda (_: C).(\lambda (v: T).(let
-TMP_124 \def (r k d) in (let TMP_125 \def (lift h0 TMP_124 v) in (eq T u
-TMP_125))))) in (let TMP_128 \def (\lambda (e0: C).(\lambda (_: T).(let
-TMP_127 \def (r k d) in (drop h0 TMP_127 c e0)))) in (ex3_2 C T TMP_123
-TMP_126 TMP_128))))))) in (let H11 \def (eq_ind C c0 TMP_129 H3 c H10) in
-(let TMP_131 \def (\lambda (c1: C).(let TMP_130 \def (r k0 d0) in (drop h0
-TMP_130 c1 e))) in (let H12 \def (eq_ind C c0 TMP_131 H2 c H10) in (let
-TMP_134 \def (\lambda (k1: K).(let TMP_132 \def (r k1 d0) in (let TMP_133
-\def (lift h0 TMP_132 u0) in (eq T TMP_133 u)))) in (let H13 \def (eq_ind K
-k0 TMP_134 H8 k H9) in (let TMP_142 \def (\lambda (k1: K).((eq nat (r k1 d0)
-(S d)) \to ((eq C c (CHead c k u)) \to (let TMP_136 \def (\lambda (e0:
-C).(\lambda (v: T).(let TMP_135 \def (CHead e0 k v) in (eq C e TMP_135)))) in
-(let TMP_139 \def (\lambda (_: C).(\lambda (v: T).(let TMP_137 \def (r k d)
-in (let TMP_138 \def (lift h0 TMP_137 v) in (eq T u TMP_138))))) in (let
-TMP_141 \def (\lambda (e0: C).(\lambda (_: T).(let TMP_140 \def (r k d) in
-(drop h0 TMP_140 c e0)))) in (ex3_2 C T TMP_136 TMP_139 TMP_141))))))) in
-(let H14 \def (eq_ind K k0 TMP_142 H11 k H9) in (let TMP_144 \def (\lambda
-(k1: K).(let TMP_143 \def (r k1 d0) in (drop h0 TMP_143 c e))) in (let H15
-\def (eq_ind K k0 TMP_144 H12 k H9) in (let TMP_153 \def (\lambda (k1:
-K).(let TMP_147 \def (\lambda (e0: C).(\lambda (v: T).(let TMP_145 \def
-(CHead e k1 u0) in (let TMP_146 \def (CHead e0 k v) in (eq C TMP_145
-TMP_146))))) in (let TMP_150 \def (\lambda (_: C).(\lambda (v: T).(let
-TMP_148 \def (r k d) in (let TMP_149 \def (lift h0 TMP_148 v) in (eq T u
-TMP_149))))) in (let TMP_152 \def (\lambda (e0: C).(\lambda (_: T).(let
-TMP_151 \def (r k d) in (drop h0 TMP_151 c e0)))) in (ex3_2 C T TMP_147
-TMP_150 TMP_152))))) in (let TMP_161 \def (\lambda (t: T).((eq nat (r k d0)
-(S d)) \to ((eq C c (CHead c k t)) \to (let TMP_155 \def (\lambda (e0:
-C).(\lambda (v: T).(let TMP_154 \def (CHead e0 k v) in (eq C e TMP_154)))) in
-(let TMP_158 \def (\lambda (_: C).(\lambda (v: T).(let TMP_156 \def (r k d)
-in (let TMP_157 \def (lift h0 TMP_156 v) in (eq T t TMP_157))))) in (let
-TMP_160 \def (\lambda (e0: C).(\lambda (_: T).(let TMP_159 \def (r k d) in
-(drop h0 TMP_159 c e0)))) in (ex3_2 C T TMP_155 TMP_158 TMP_160))))))) in
-(let TMP_162 \def (r k d0) in (let TMP_163 \def (lift h0 TMP_162 u0) in (let
-H16 \def (eq_ind_r T u TMP_161 H14 TMP_163 H13) in (let TMP_164 \def (r k d0)
-in (let TMP_165 \def (lift h0 TMP_164 u0) in (let TMP_174 \def (\lambda (t:
-T).(let TMP_168 \def (\lambda (e0: C).(\lambda (v: T).(let TMP_166 \def
-(CHead e k u0) in (let TMP_167 \def (CHead e0 k v) in (eq C TMP_166
-TMP_167))))) in (let TMP_171 \def (\lambda (_: C).(\lambda (v: T).(let
-TMP_169 \def (r k d) in (let TMP_170 \def (lift h0 TMP_169 v) in (eq T t
-TMP_170))))) in (let TMP_173 \def (\lambda (e0: C).(\lambda (_: T).(let
-TMP_172 \def (r k d) in (drop h0 TMP_172 c e0)))) in (ex3_2 C T TMP_168
-TMP_171 TMP_173))))) in (let TMP_175 \def (\lambda (e0: nat).(match e0 with
-[O \Rightarrow d0 | (S n) \Rightarrow n])) in (let TMP_176 \def (S d0) in
-(let TMP_177 \def (S d) in (let H17 \def (f_equal nat nat TMP_175 TMP_176
-TMP_177 H4) in (let TMP_187 \def (\lambda (n: nat).((eq nat (r k n) (S d))
-\to ((eq C c (CHead c k (lift h0 (r k n) u0))) \to (let TMP_179 \def (\lambda
-(e0: C).(\lambda (v: T).(let TMP_178 \def (CHead e0 k v) in (eq C e
-TMP_178)))) in (let TMP_184 \def (\lambda (_: C).(\lambda (v: T).(let TMP_180
-\def (r k n) in (let TMP_181 \def (lift h0 TMP_180 u0) in (let TMP_182 \def
-(r k d) in (let TMP_183 \def (lift h0 TMP_182 v) in (eq T TMP_181
-TMP_183))))))) in (let TMP_186 \def (\lambda (e0: C).(\lambda (_: T).(let
-TMP_185 \def (r k d) in (drop h0 TMP_185 c e0)))) in (ex3_2 C T TMP_179
-TMP_184 TMP_186))))))) in (let H18 \def (eq_ind nat d0 TMP_187 H16 d H17) in
-(let TMP_189 \def (\lambda (n: nat).(let TMP_188 \def (r k n) in (drop h0
-TMP_188 c e))) in (let H19 \def (eq_ind nat d0 TMP_189 H15 d H17) in (let
-TMP_200 \def (\lambda (n: nat).(let TMP_192 \def (\lambda (e0: C).(\lambda
-(v: T).(let TMP_190 \def (CHead e k u0) in (let TMP_191 \def (CHead e0 k v)
-in (eq C TMP_190 TMP_191))))) in (let TMP_197 \def (\lambda (_: C).(\lambda
-(v: T).(let TMP_193 \def (r k n) in (let TMP_194 \def (lift h0 TMP_193 u0) in
-(let TMP_195 \def (r k d) in (let TMP_196 \def (lift h0 TMP_195 v) in (eq T
-TMP_194 TMP_196))))))) in (let TMP_199 \def (\lambda (e0: C).(\lambda (_:
-T).(let TMP_198 \def (r k d) in (drop h0 TMP_198 c e0)))) in (ex3_2 C T
-TMP_192 TMP_197 TMP_199))))) in (let TMP_203 \def (\lambda (e0: C).(\lambda
-(v: T).(let TMP_201 \def (CHead e k u0) in (let TMP_202 \def (CHead e0 k v)
-in (eq C TMP_201 TMP_202))))) in (let TMP_208 \def (\lambda (_: C).(\lambda
-(v: T).(let TMP_204 \def (r k d) in (let TMP_205 \def (lift h0 TMP_204 u0) in
-(let TMP_206 \def (r k d) in (let TMP_207 \def (lift h0 TMP_206 v) in (eq T
-TMP_205 TMP_207))))))) in (let TMP_210 \def (\lambda (e0: C).(\lambda (_:
-T).(let TMP_209 \def (r k d) in (drop h0 TMP_209 c e0)))) in (let TMP_211
-\def (CHead e k u0) in (let TMP_212 \def (refl_equal C TMP_211) in (let
-TMP_213 \def (r k d) in (let TMP_214 \def (lift h0 TMP_213 u0) in (let
-TMP_215 \def (refl_equal T TMP_214) in (let TMP_216 \def (ex3_2_intro C T
-TMP_203 TMP_208 TMP_210 e u0 TMP_212 TMP_215 H19) in (let TMP_217 \def
-(eq_ind_r nat d TMP_200 TMP_216 d0 H17) in (let TMP_218 \def (eq_ind T
-TMP_165 TMP_174 TMP_217 u H13) in (eq_ind_r K k TMP_153 TMP_218 k0
-H9))))))))))))))))))))))))))))))))))))))))) in (let TMP_220 \def (TMP_219 H7)
-in (TMP_220 H6))))))))))))))))))))))))))))))) in (drop_ind TMP_29 TMP_51
-TMP_99 TMP_221 h y0 y x H1))))))) in (insert_eq nat TMP_12 TMP_13 TMP_21
-TMP_222 H0))))))) in (insert_eq C TMP_1 TMP_3 TMP_11 TMP_223 H))))))))))).
+(_: T).(drop h0 (r k d) c e0))))) (let H16 \def (eq_ind_r T u (\lambda (t:
+T).((eq nat (r k d0) (S d)) \to ((eq C c (CHead c k t)) \to (ex3_2 C T
+(\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 k v)))) (\lambda (_:
+C).(\lambda (v: T).(eq T t (lift h0 (r k d) v)))) (\lambda (e0: C).(\lambda
+(_: T).(drop h0 (r k d) c e0))))))) H14 (lift h0 (r k d0) u0) H13) in (eq_ind
+T (lift h0 (r k d0) u0) (\lambda (t: T).(ex3_2 C T (\lambda (e0: C).(\lambda
+(v: T).(eq C (CHead e k u0) (CHead e0 k v)))) (\lambda (_: C).(\lambda (v:
+T).(eq T t (lift h0 (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h0
+(r k d) c e0))))) (let H17 \def (f_equal nat nat (\lambda (e0: nat).(match e0
+with [O \Rightarrow d0 | (S n) \Rightarrow n])) (S d0) (S d) H4) in (let H18
+\def (eq_ind nat d0 (\lambda (n: nat).((eq nat (r k n) (S d)) \to ((eq C c
+(CHead c k (lift h0 (r k n) u0))) \to (ex3_2 C T (\lambda (e0: C).(\lambda
+(v: T).(eq C e (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T (lift
+h0 (r k n) u0) (lift h0 (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop
+h0 (r k d) c e0))))))) H16 d H17) in (let H19 \def (eq_ind nat d0 (\lambda
+(n: nat).(drop h0 (r k n) c e)) H15 d H17) in (eq_ind_r nat d (\lambda (n:
+nat).(ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C (CHead e k u0) (CHead
+e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T (lift h0 (r k n) u0) (lift
+h0 (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h0 (r k d) c e0)))))
+(ex3_2_intro C T (\lambda (e0: C).(\lambda (v: T).(eq C (CHead e k u0) (CHead
+e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T (lift h0 (r k d) u0) (lift
+h0 (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h0 (r k d) c e0))) e
+u0 (refl_equal C (CHead e k u0)) (refl_equal T (lift h0 (r k d) u0)) H19) d0
+H17)))) u H13)) k0 H9))))))))) H7)) H6)))))))))))) h y0 y x H1))) H0)))
+H))))))).