I am trying to generate models for the following sequent.
$$\exists x \exists y \forall z (z = x \lor z = y)$$
What I have come up with is this.
So in this model, for all the values of $z$ there exists $x$ such that $z = x$ or there exists $y$ such that $z = y$. Is this model correct? What other models are there that satisfy this?