TODO (113B)
1 Document FinatSeq 2 3 FinaturalSeq, or somehow generalize FinatSeq to support other IsFin types 4 5 Add version number