This starts the work on #108 by implementing insert and index for Z as well as lengthZ, takeZ, dropZ, and porting much of the associated theory.
I have not ported everything, e.g. the interactions with Forall3, subseteq, submseteq, filter, mask are missing. Also there are more operations that would need a Z-based version, such as lookup_total, alter, delete, inserts, find, imap, imap2, resize, rotate, rotate_take, sublist_lookup, sublist_alter. There are also some tactics that will not handle these new operations and so might need adjustments or Z-based tactics: solve_length, simplify_list_eq.
Still I think this is a useful start that can serve as a foundation for later extensions. :)
Blocked on !441 (merged).