WIP: Some lemmas about `list_lookup_total`

Partially addresses #50 (closed)

marked as a Work In Progress

Discussed this with @dfrumin in private; there are still plenty of lemmas missing, we should go systematically over all lemmas involving lookup (basically do a search in the file for !!).

Another thing we discussed in private, some lemmas like:

Lemma list_lookup_total_insert `{!Inhabited A} l i x :
  i < length l → <[i:=x]>l !!! i = x.

Need a side-condition. You can either use is_Some (l !!! i) or i < length l. Both are logically equivalent, but @dfrumin pointed out that the former can, in some cases, be automatically discharged by lia or it may be preferred.

mentioned in merge request !125 (merged)

closed

Closing in favor of !125 (merged).