(H4: (drop1 p x e)).(eq_ind_r TList (lifts n n0 (lifts1 p ts)) (\lambda (t:
TList).(sns3 c t)) (sns3_lifts c x n n0 H3 (lifts1 p ts) (H x H4 ts H1))
(lifts1 (PCons n n0 p) ts) (lifts1_cons n n0 p ts))))) H2))))))))))) hds)).
(H4: (drop1 p x e)).(eq_ind_r TList (lifts n n0 (lifts1 p ts)) (\lambda (t:
TList).(sns3 c t)) (sns3_lifts c x n n0 H3 (lifts1 p ts) (H x H4 ts H1))
(lifts1 (PCons n n0 p) ts) (lifts1_cons n n0 p ts))))) H2))))))))))) hds)).