More work on MMorph
Added a basic framework for set theory

Taken from Formal Construction of a Set Theory in Coq, by Jonas Jaiser.
The proofs are my own, I just needed a framework to start with.