Major update:

- Added AlgebraTheory.agda, FinTheory.agda, and Finite.agda
- NFA.agda is now NFA-epsilon.agda
- Finite.agda deals with setoids which have finitely many distinct elements
- Removed the algebraic structures for sets, but added a lattice structure
- NFA sets no longer need be decidable
- NFA states can now be any type with finitely many members
- Added a combinator for NFA union along with a proof of its correctness