feat(data/{list/alist,finmap}): implicit key type (#662)
* feat(data/{list/alist,finmap}): implicit key type
Make the key type α implicit in both alist and finmap. This brings these
types into line with the underlying sigma and simplifies usage since α
is inferred from the value function type β : α → Type v.
* doc(data/list/alist): alist is stored as a linked list
