- \lambda (x2: C).(let TMP_6 \def (\lambda (c: C).(\forall (x1: C).(\forall
-(h: nat).(\forall (d: nat).((drop h (S d) x1 c) \to (\forall (b: B).(\forall
-(c2: C).(\forall (u: T).((clear c (CHead c2 (Bind b) u)) \to (let TMP_4 \def
-(\lambda (c1: C).(let TMP_1 \def (Bind b) in (let TMP_2 \def (lift h d u) in
-(let TMP_3 \def (CHead c1 TMP_1 TMP_2) in (clear x1 TMP_3))))) in (let TMP_5
-\def (\lambda (c1: C).(drop h d c1 c2)) in (ex2 C TMP_4 TMP_5)))))))))))) in
-(let TMP_15 \def (\lambda (n: nat).(\lambda (x1: C).(\lambda (h:
-nat).(\lambda (d: nat).(\lambda (_: (drop h (S d) x1 (CSort n))).(\lambda (b:
-B).(\lambda (c2: C).(\lambda (u: T).(\lambda (H0: (clear (CSort n) (CHead c2
-(Bind b) u))).(let TMP_7 \def (Bind b) in (let TMP_8 \def (CHead c2 TMP_7 u)
-in (let TMP_12 \def (\lambda (c1: C).(let TMP_9 \def (Bind b) in (let TMP_10
-\def (lift h d u) in (let TMP_11 \def (CHead c1 TMP_9 TMP_10) in (clear x1
-TMP_11))))) in (let TMP_13 \def (\lambda (c1: C).(drop h d c1 c2)) in (let
-TMP_14 \def (ex2 C TMP_12 TMP_13) in (clear_gen_sort TMP_8 n H0
-TMP_14))))))))))))))) in (let TMP_162 \def (\lambda (c: C).(\lambda (H:
-((\forall (x1: C).(\forall (h: nat).(\forall (d: nat).((drop h (S d) x1 c)
-\to (\forall (b: B).(\forall (c2: C).(\forall (u: T).((clear c (CHead c2
-(Bind b) u)) \to (ex2 C (\lambda (c1: C).(clear x1 (CHead c1 (Bind b) (lift h
-d u)))) (\lambda (c1: C).(drop h d c1 c2))))))))))))).(\lambda (k:
-K).(\lambda (t: T).(\lambda (x1: C).(\lambda (h: nat).(\lambda (d:
-nat).(\lambda (H0: (drop h (S d) x1 (CHead c k t))).(\lambda (b: B).(\lambda
-(c2: C).(\lambda (u: T).(\lambda (H1: (clear (CHead c k t) (CHead c2 (Bind b)
-u))).(let TMP_19 \def (\lambda (e: C).(let TMP_16 \def (r k d) in (let TMP_17
-\def (lift h TMP_16 t) in (let TMP_18 \def (CHead e k TMP_17) in (eq C x1
-TMP_18))))) in (let TMP_21 \def (\lambda (e: C).(let TMP_20 \def (r k d) in
-(drop h TMP_20 e c))) in (let TMP_25 \def (\lambda (c1: C).(let TMP_22 \def
-(Bind b) in (let TMP_23 \def (lift h d u) in (let TMP_24 \def (CHead c1
-TMP_22 TMP_23) in (clear x1 TMP_24))))) in (let TMP_26 \def (\lambda (c1:
-C).(drop h d c1 c2)) in (let TMP_27 \def (ex2 C TMP_25 TMP_26) in (let
-TMP_160 \def (\lambda (x: C).(\lambda (H2: (eq C x1 (CHead x k (lift h (r k
-d) t)))).(\lambda (H3: (drop h (r k d) x c)).(let TMP_28 \def (r k d) in (let
-TMP_29 \def (lift h TMP_28 t) in (let TMP_30 \def (CHead x k TMP_29) in (let
-TMP_36 \def (\lambda (c0: C).(let TMP_34 \def (\lambda (c1: C).(let TMP_31
-\def (Bind b) in (let TMP_32 \def (lift h d u) in (let TMP_33 \def (CHead c1
-TMP_31 TMP_32) in (clear c0 TMP_33))))) in (let TMP_35 \def (\lambda (c1:
-C).(drop h d c1 c2)) in (ex2 C TMP_34 TMP_35)))) in (let TMP_45 \def (\lambda
-(k0: K).((clear (CHead c k0 t) (CHead c2 (Bind b) u)) \to ((drop h (r k0 d) x
-c) \to (let TMP_43 \def (\lambda (c1: C).(let TMP_37 \def (r k0 d) in (let
-TMP_38 \def (lift h TMP_37 t) in (let TMP_39 \def (CHead x k0 TMP_38) in (let
-TMP_40 \def (Bind b) in (let TMP_41 \def (lift h d u) in (let TMP_42 \def
-(CHead c1 TMP_40 TMP_41) in (clear TMP_39 TMP_42)))))))) in (let TMP_44 \def
-(\lambda (c1: C).(drop h d c1 c2)) in (ex2 C TMP_43 TMP_44)))))) in (let
-TMP_120 \def (\lambda (b0: B).(\lambda (H4: (clear (CHead c (Bind b0) t)
-(CHead c2 (Bind b) u))).(\lambda (H5: (drop h (r (Bind b0) d) x c)).(let
-TMP_46 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow c2 | (CHead
-c0 _ _) \Rightarrow c0])) in (let TMP_47 \def (Bind b) in (let TMP_48 \def
-(CHead c2 TMP_47 u) in (let TMP_49 \def (Bind b0) in (let TMP_50 \def (CHead
-c TMP_49 t) in (let TMP_51 \def (Bind b) in (let TMP_52 \def (CHead c2 TMP_51
-u) in (let TMP_53 \def (clear_gen_bind b0 c TMP_52 t H4) in (let H6 \def
-(f_equal C C TMP_46 TMP_48 TMP_50 TMP_53) in (let TMP_54 \def (\lambda (e:
+ \lambda (x2: C).(C_ind (\lambda (c: C).(\forall (x1: C).(\forall (h:
+nat).(\forall (d: nat).((drop h (S d) x1 c) \to (\forall (b: B).(\forall (c2:
+C).(\forall (u: T).((clear c (CHead c2 (Bind b) u)) \to (ex2 C (\lambda (c1:
+C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1
+c2)))))))))))) (\lambda (n: nat).(\lambda (x1: C).(\lambda (h: nat).(\lambda
+(d: nat).(\lambda (_: (drop h (S d) x1 (CSort n))).(\lambda (b: B).(\lambda
+(c2: C).(\lambda (u: T).(\lambda (H0: (clear (CSort n) (CHead c2 (Bind b)
+u))).(clear_gen_sort (CHead c2 (Bind b) u) n H0 (ex2 C (\lambda (c1:
+C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1
+c2))))))))))))) (\lambda (c: C).(\lambda (H: ((\forall (x1: C).(\forall (h:
+nat).(\forall (d: nat).((drop h (S d) x1 c) \to (\forall (b: B).(\forall (c2:
+C).(\forall (u: T).((clear c (CHead c2 (Bind b) u)) \to (ex2 C (\lambda (c1:
+C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1
+c2))))))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (x1: C).(\lambda (h:
+nat).(\lambda (d: nat).(\lambda (H0: (drop h (S d) x1 (CHead c k
+t))).(\lambda (b: B).(\lambda (c2: C).(\lambda (u: T).(\lambda (H1: (clear
+(CHead c k t) (CHead c2 (Bind b) u))).(ex2_ind C (\lambda (e: C).(eq C x1
+(CHead e k (lift h (r k d) t)))) (\lambda (e: C).(drop h (r k d) e c)) (ex2 C
+(\lambda (c1: C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1:
+C).(drop h d c1 c2))) (\lambda (x: C).(\lambda (H2: (eq C x1 (CHead x k (lift
+h (r k d) t)))).(\lambda (H3: (drop h (r k d) x c)).(eq_ind_r C (CHead x k
+(lift h (r k d) t)) (\lambda (c0: C).(ex2 C (\lambda (c1: C).(clear c0 (CHead
+c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2)))) (K_ind
+(\lambda (k0: K).((clear (CHead c k0 t) (CHead c2 (Bind b) u)) \to ((drop h
+(r k0 d) x c) \to (ex2 C (\lambda (c1: C).(clear (CHead x k0 (lift h (r k0 d)
+t)) (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2))))))
+(\lambda (b0: B).(\lambda (H4: (clear (CHead c (Bind b0) t) (CHead c2 (Bind
+b) u))).(\lambda (H5: (drop h (r (Bind b0) d) x c)).(let H6 \def (f_equal C C
+(\lambda (e: C).(match e with [(CSort _) \Rightarrow c2 | (CHead c0 _ _)
+\Rightarrow c0])) (CHead c2 (Bind b) u) (CHead c (Bind b0) t) (clear_gen_bind
+b0 c (CHead c2 (Bind b) u) t H4)) in ((let H7 \def (f_equal C B (\lambda (e: