Theorems and lemmas for dealing with List.ofFn, which converts a function on Fin n to a list
of length n.
The main statements pertain to lists generated using List.ofFn
The length of a list converted from a function is the size of the domain.
The nth element of a list
ofFn on an empty domain is the empty list.
Note this matches the convention of List.ofFn_succ', putting the Fin m elements first.
This breaks a list of m*n items into m groups each containing n elements.
This breaks a list of m*n items into n groups each containing m elements.
Lists are equivalent to the sigma type of tuples of a given length.
A recursor for lists that expands a list into a function mapping to its elements.
This can be used with induction l using List.ofFnRec.
induction l using List.ofFnRec
Fin.sigma_eq_iff_eq_comp_cast may be useful to work with the RHS of this expression.
Note we can only state this when the two functions are indexed by defeq n.
A special case of List.ofFn_inj for when the two functions are indexed by defeq n.