- \lambda (b: B).(\lambda (e: C).(\lambda (hds: PList).(let TMP_7 \def
-(\lambda (p: PList).(\forall (c: C).(\forall (u: T).((drop1 p c e) \to (let
-TMP_1 \def (Ss p) in (let TMP_2 \def (Bind b) in (let TMP_3 \def (lift1 p u)
-in (let TMP_4 \def (CHead c TMP_2 TMP_3) in (let TMP_5 \def (Bind b) in (let
-TMP_6 \def (CHead e TMP_5 u) in (drop1 TMP_1 TMP_4 TMP_6))))))))))) in (let
-TMP_16 \def (\lambda (c: C).(\lambda (u: T).(\lambda (H: (drop1 PNil c
-e)).(let H_y \def (drop1_gen_pnil c e H) in (let TMP_12 \def (\lambda (c0:
-C).(let TMP_8 \def (Bind b) in (let TMP_9 \def (CHead c0 TMP_8 u) in (let
-TMP_10 \def (Bind b) in (let TMP_11 \def (CHead e TMP_10 u) in (drop1 PNil
-TMP_9 TMP_11)))))) in (let TMP_13 \def (Bind b) in (let TMP_14 \def (CHead e
-TMP_13 u) in (let TMP_15 \def (drop1_nil TMP_14) in (eq_ind_r C e TMP_12
-TMP_15 c H_y))))))))) in (let TMP_44 \def (\lambda (n: nat).(\lambda (n0:
-nat).(\lambda (p: PList).(\lambda (H: ((\forall (c: C).(\forall (u:
-T).((drop1 p c e) \to (drop1 (Ss p) (CHead c (Bind b) (lift1 p u)) (CHead e
-(Bind b) u))))))).(\lambda (c: C).(\lambda (u: T).(\lambda (H0: (drop1 (PCons
-n n0 p) c e)).(let H_x \def (drop1_gen_pcons c e p n n0 H0) in (let H1 \def
-H_x in (let TMP_17 \def (\lambda (c2: C).(drop n n0 c c2)) in (let TMP_18
-\def (\lambda (c2: C).(drop1 p c2 e)) in (let TMP_19 \def (S n0) in (let
-TMP_20 \def (Ss p) in (let TMP_21 \def (PCons n TMP_19 TMP_20) in (let TMP_22
-\def (Bind b) in (let TMP_23 \def (lift1 p u) in (let TMP_24 \def (lift n n0
-TMP_23) in (let TMP_25 \def (CHead c TMP_22 TMP_24) in (let TMP_26 \def (Bind
-b) in (let TMP_27 \def (CHead e TMP_26 u) in (let TMP_28 \def (drop1 TMP_21
-TMP_25 TMP_27) in (let TMP_43 \def (\lambda (x: C).(\lambda (H2: (drop n n0 c
-x)).(\lambda (H3: (drop1 p x e)).(let TMP_29 \def (Bind b) in (let TMP_30
-\def (lift1 p u) in (let TMP_31 \def (lift n n0 TMP_30) in (let TMP_32 \def
-(CHead c TMP_29 TMP_31) in (let TMP_33 \def (Bind b) in (let TMP_34 \def
-(lift1 p u) in (let TMP_35 \def (CHead x TMP_33 TMP_34) in (let TMP_36 \def
-(S n0) in (let TMP_37 \def (lift1 p u) in (let TMP_38 \def (drop_skip_bind n
-n0 c x H2 b TMP_37) in (let TMP_39 \def (Bind b) in (let TMP_40 \def (CHead e
-TMP_39 u) in (let TMP_41 \def (Ss p) in (let TMP_42 \def (H x u H3) in
-(drop1_cons TMP_32 TMP_35 n TMP_36 TMP_38 TMP_40 TMP_41
-TMP_42)))))))))))))))))) in (ex2_ind C TMP_17 TMP_18 TMP_28 TMP_43
-H1))))))))))))))))))))))) in (PList_ind TMP_7 TMP_16 TMP_44 hds)))))).
+ \lambda (b: B).(\lambda (e: C).(\lambda (hds: PList).(PList_ind (\lambda (p:
+PList).(\forall (c: C).(\forall (u: T).((drop1 p c e) \to (drop1 (Ss p)
+(CHead c (Bind b) (lift1 p u)) (CHead e (Bind b) u)))))) (\lambda (c:
+C).(\lambda (u: T).(\lambda (H: (drop1 PNil c e)).(let H_y \def
+(drop1_gen_pnil c e H) in (eq_ind_r C e (\lambda (c0: C).(drop1 PNil (CHead
+c0 (Bind b) u) (CHead e (Bind b) u))) (drop1_nil (CHead e (Bind b) u)) c
+H_y))))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda
+(H: ((\forall (c: C).(\forall (u: T).((drop1 p c e) \to (drop1 (Ss p) (CHead
+c (Bind b) (lift1 p u)) (CHead e (Bind b) u))))))).(\lambda (c: C).(\lambda
+(u: T).(\lambda (H0: (drop1 (PCons n n0 p) c e)).(let H_x \def
+(drop1_gen_pcons c e p n n0 H0) in (let H1 \def H_x in (ex2_ind C (\lambda
+(c2: C).(drop n n0 c c2)) (\lambda (c2: C).(drop1 p c2 e)) (drop1 (PCons n (S
+n0) (Ss p)) (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead e (Bind b) u))
+(\lambda (x: C).(\lambda (H2: (drop n n0 c x)).(\lambda (H3: (drop1 p x
+e)).(drop1_cons (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead x (Bind b)
+(lift1 p u)) n (S n0) (drop_skip_bind n n0 c x H2 b (lift1 p u)) (CHead e
+(Bind b) u) (Ss p) (H x u H3))))) H1)))))))))) hds))).