Makes rndFin take all values in Fin (S k)

Previously, rndFin k only took values in 0, 1, ... , k - 1, even
though the type Fin (S k) has elements 0, 1, ..., k.
Adds docstrings
Adds rndSelect

Adds functions to select random elements from lists and vectors.
These functions also demonstrate the naturalness of the new definition
of rndFin.