nat).(\lambda (d: nat).(eq_ind_r T (THead k (lift i d v) (lift i (s k d) t0))
(\lambda (t1: T).(cnt t1)) (cnt_head (lift i (s k d) t0) (H1 i (s k d)) k
(lift i d v)) (lift i d (THead k v t0)) (lift_head k v t0 i d))))))))) t H)).
nat).(\lambda (d: nat).(eq_ind_r T (THead k (lift i d v) (lift i (s k d) t0))
(\lambda (t1: T).(cnt t1)) (cnt_head (lift i (s k d) t0) (H1 i (s k d)) k
(lift i d v)) (lift i d (THead k v t0)) (lift_head k v t0 i d))))))))) t H)).