So, thin is a dependently typed recursive functional.
Note that the recursive call is only well typed because fs i is in fin at least 2.
Next: thickening a finite set | Prev: thin at fs | Up: contents