feat: An initial version of Buchi and Muller automata

[ctchou]

This patch shows what the definitions of Büchi and Muller automata will look like. It depends on the following two PRs:
#80
#83

One thing that will likely to change is that instead of directly using Set (List Symbol) and Set (ωList Symbol) to represent languages and ω-languages, we will define types Language Symbol and ωLanguage Symbol to wrap them, in the style of mathlib:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/Language.html

[ctchou]

Rebase on the current "main".