Merge Fin.Data and Fin.Data.Inductive

[mortberg]

There is currently some unnecessary duplication between Data.Fin and Data.Fin.Inductive. These two definitions of Fin are almost identical, but parts of the library uses one definition and some uses the other.

@aljungstrom has convinced me that version one in Data.Fin.Inductive is better as it satisfies more definitional equalities, so I suggest we put that version in Data.Fin and use it everywhere. @croos90 is currently working on implementing this, so this issue is mostly here to avoid someone else starting to work on the same thing.

[mortberg]

In the future we also plan to remove some dependencies on Data.FinData as inductive families are poorly supported in Cubical Agda and it would be better to use Data.Fin throughout instead. Dependencies I have in mind are matrices and big operators. I will make a separate issue with a more detailed plan for that once the current issue has been fixed.