Provide a total version of `!!` for finite maps and lists

In case the type is inhabited, we can define a total version of the lookup function as follows:

l !!! i = match l !! i with Some x => x | None => inhabitant end

Having such a total lookup function is often convenient. It came up in some discussions with Arthur and also @dfrumin requested having such a feature recently.

I would like to implement this by defining a type class LookupTotal with its own notation (suggestion !!!) and then have instances and lemmas for all of the usual data structures like maps and lists. For maps, we can define an instance like the above. For lists I would like to have an instance that is not just m !!! i = if m !! i is Some x then x else inhabitant but something that is defined by structural recursion, so you can use it more easily in induction proofs.

We could furthermore provide an instance LookupTotal (vec A n) (fin n) A for vectors. This operation is always total, regardless of whether A is inhabited. Note that we already use the notation !!! for vectors, so generalizing it to the type class based version as proposed here makes sense.