Finite Sets

I noticed, that I need finite sets of letters, variables and rules for grammars and languages.

A look on Coq.Logic.FinFun could be a good idea.