I had to work with lists a lot, so I needed lemmas about their local updates.
option_local_update' is part of this MR because I didn't find any other use for it. Maybe its proof can be simplified and inlined, but I couldn't find a way.
There is a lot in this MR, and I am sure that much of this could be done in a significantly better way, so I didn't yet ensure that the style is satisfactory. I would appreciate it if we could discuss the statements of lemmas and the general approach before I tidy up the final design.