-(drop1_getl_trans is c d0 H7 Abbr d v i H2) in (let H8 \def H_x in (ex_ind C
-(\lambda (e2: C).(getl (trans is i) d0 (CHead e2 (Bind Abbr) (ctrans is i
-v)))) (sc3 g a1 d0 (THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs
-(TLRef i))))) (\lambda (x: C).(\lambda (H9: (getl (trans is i) d0 (CHead x
-(Bind Abbr) (ctrans is i v)))).(let H_y \def (H0 (TCons w (lifts1 is vs))) in
-(eq_ind_r T (THeads (Flat Appl) (lifts1 is vs) (lift1 is (TLRef i))) (\lambda
-(t: T).(sc3 g a1 d0 (THead (Flat Appl) w t))) (eq_ind_r T (TLRef (trans is
-i)) (\lambda (t: T).(sc3 g a1 d0 (THead (Flat Appl) w (THeads (Flat Appl)
-(lifts1 is vs) t)))) (H_y (trans is i) x (ctrans is i v) d0 (eq_ind T (lift1
-is (lift (S i) O v)) (\lambda (t: T).(sc3 g a1 d0 (THead (Flat Appl) w
-(THeads (Flat Appl) (lifts1 is vs) t)))) (eq_ind T (lift1 is (THeads (Flat
-Appl) vs (lift (S i) O v))) (\lambda (t: T).(sc3 g a1 d0 (THead (Flat Appl) w
-t))) (H5 d0 w H6 is H7) (THeads (Flat Appl) (lifts1 is vs) (lift1 is (lift (S
-i) O v))) (lifts1_flat Appl is (lift (S i) O v) vs)) (lift (S (trans is i)) O
-(ctrans is i v)) (lift1_free is i v)) H9) (lift1 is (TLRef i)) (lift1_lref is
-i)) (lift1 is (THeads (Flat Appl) vs (TLRef i))) (lifts1_flat Appl is (TLRef
-i) vs))))) H8))))))))))) H3))))))))))))) a)).
+(drop1_getl_trans is c d0 H7 Abbr d v i H2) in (let H8 \def H_x in (ex2_ind C
+(\lambda (e2: C).(drop1 (ptrans is i) e2 d)) (\lambda (e2: C).(getl (trans is
+i) d0 (CHead e2 (Bind Abbr) (lift1 (ptrans is i) v)))) (sc3 g a1 d0 (THead
+(Flat Appl) w (lift1 is (THeads (Flat Appl) vs (TLRef i))))) (\lambda (x:
+C).(\lambda (_: (drop1 (ptrans is i) x d)).(\lambda (H10: (getl (trans is i)
+d0 (CHead x (Bind Abbr) (lift1 (ptrans is i) v)))).(let H_y \def (H0 (TCons w
+(lifts1 is vs))) in (eq_ind_r T (THeads (Flat Appl) (lifts1 is vs) (lift1 is
+(TLRef i))) (\lambda (t: T).(sc3 g a1 d0 (THead (Flat Appl) w t))) (eq_ind_r
+T (TLRef (trans is i)) (\lambda (t: T).(sc3 g a1 d0 (THead (Flat Appl) w
+(THeads (Flat Appl) (lifts1 is vs) t)))) (H_y (trans is i) x (lift1 (ptrans
+is i) v) d0 (eq_ind T (lift1 is (lift (S i) O v)) (\lambda (t: T).(sc3 g a1
+d0 (THead (Flat Appl) w (THeads (Flat Appl) (lifts1 is vs) t)))) (eq_ind T
+(lift1 is (THeads (Flat Appl) vs (lift (S i) O v))) (\lambda (t: T).(sc3 g a1
+d0 (THead (Flat Appl) w t))) (H5 d0 w H6 is H7) (THeads (Flat Appl) (lifts1
+is vs) (lift1 is (lift (S i) O v))) (lifts1_flat Appl is (lift (S i) O v)
+vs)) (lift (S (trans is i)) O (lift1 (ptrans is i) v)) (lift1_free is i v))
+H10) (lift1 is (TLRef i)) (lift1_lref is i)) (lift1 is (THeads (Flat Appl) vs
+(TLRef i))) (lifts1_flat Appl is (TLRef i) vs)))))) H8)))))))))))
+H3))))))))))))) a)).