I'm reading Fitting's Intuitionistic Logic, Model Theory and Forcing. This occurs in Chapter 7.15.
The aim is to prove that a certain intuitionistic model is an intuitionistic model of ZF. I unfortunately don't think I can sum up what is happening to someone unfamiliar with the book at all, so I will simply post a screenshot of what Fitting does and hope someone here has worked through it before.
I'm concerned about this lemma that he states right at the beginning of the chapter (the image shows both the statement and the proof). I understand the proof completely, but I don't see why we require that $\Gamma^* \vDash ((t \in c_1) \leftrightarrow (t \in c_2))$ at all. After all, we're dealing with an intuitionistic Kripke model, so we could just require that $\Gamma \vDash ((t \in c_1) \leftrightarrow (t \in c_2))$ and this should follow immediately.
Fitting usually doesn't make an error like this and he actually repeats it on the next page and emphasizes it's important to look at every successor $\Gamma^*$, so I guess I must be missing something. The only thing I can think of is that the domain of $t$ changes throughout the model, but it really shouldn't, as all $t$-s are from a fixed $\rho_{\alpha_0}$.