Theorems and lemmas for dealing with list.of_fn, which converts a function on fin n to a list
of length n.
The main definitions pertain to lists generated using of_fn
The length of a list converted from a function is the size of the domain.
The nth element of a list
Arrays converted to lists are the same as of_fn on the indexing function of the array.
of_fn on an empty domain is the empty list.