Adjusted the end of Lemma 3.2.B so that it doesn’t rely on on axiom3b. It now follows more closely to Street’s argument.

Adjusted a few random issues with unicode.
Altered tactics in mySetoids and myFiniteDefs. Shortened some proofs in those sections.
Added some hints throughout myFiniteDefs in an attempt to simplify some proofs. Made corresponding changes to ensure that all files operate as intended.