prove updates over list append

[cascade77]

This proves that updating a position over two appended character lists is equivalent to updating over each list in sequence.

[gallais]

1. This is a special case of List.fold_left_app
2. This library does not prove anything about anything (designing proof combinators to work with this set of parser combinators is a research question)

So I don't think this needs merged.