Equality of sets of local isomorphisms between relations I'm still working on the first pages of Poizat's A Course in Model Theory. I'll state the basic definitions again, in order to avoid referring back to an early question:
Poizat defines an isomorphism $s$ from a relation $R$ to a relation $R'$ as a bijection from $E$ to $E'$ (where these denote the respective underlying sets, or universes) which preserves the given relation (i.e. a sequence $\vec{a}$  satisfies $R$ iff the sequence $s(\vec{a})$ also satisfies $R'$). After defining the notion of a local isomorphism from $R$ to $R'$ as an isomorphism between finite restrictions of $R$ to $R'$ (where a finite restriction is a restriction of the relation to a finite subset of the original universe), he proceeds to define the set $S_p(R, R')$ of $p$-isomorphisms between $R$ and $R'$ ($p$ is a non-negative integer). The definition is recursive: $S_0(R,R')$ is defined as the set of all local isomorphisms between $R$ and $R'$ and, for $p\geq 0$, we say that a local isomorphism $s$ belongs to the set $S_{p+1}(R,R')$ according to the following conditions:


*

*Back: For every $a$ in the universe $E$ of $R$, there is an extension $t$ of $s$ (i.e., $\mathrm{dom}(s)\subseteq \mathrm{dom}(t)$ and $s$ is the restriction of $t$ to $\mathrm{dom}(s)$), defined at $a$, that is in $S_p(R,R')$;

*Forth: For every $b$ in the universe $E'$ of $R'$, there is an extension $t$ of $s$, whose image contains $b$, that is in $S_p(R,R')$.
Now, on page 3, he invites the reader to prove:

If, for some $p$, $S_p(R, R') = S_{p+1}(R, R')$, then, for all $q > p$, $S_p(R, R') = S_q(R, R')$.

The case where $S_p(R, R')$ is empty is trivial (it follows directly from the fact, proved by Poizat, that, for every $q > p$, $S_q(R, R') \subseteq S_p(R, R')$), so assume that it isn't empty. I've been thinking about how to prove it, but haven't gotten very far. I've thought about using induction on $q$, but I'm not sure about how to use the induction hypothesis. Any tips?
 A: The basic idea is to show that if $S_p(R,R^\prime) = S_q(R,R^\prime)$, then $S_{p+1}(R,R^\prime) = S_{q+1}(R,R^\prime)$. After this we may use the fact that $S_p (R,R^\prime) = S_{p+1} (R,R^\prime)$ to inductively conclude that $S_{q}(R,R^\prime) = S_p(R,R^\prime)$ for all $q \geq p$.
For this, suppose $s \in S_{p+1} (R,R^\prime)$, and we'll just show that it satisfying the "Back" condition for being in $S_{q+1} (R,R^\prime)$ (the "Forth" condition is essentially exactly the same).  Given $a \in E$, since $s \in S_{p+1}(R,R^\prime)$ there must be an extension $t$ of $s$ in $S_p(R,R^\prime)$ such that $a \in \operatorname{dom} (t)$. But now recall that $S_q(R,R^\prime) = S_p(R,R^\prime)$, so $t \in S_q(R,R^\prime)$.  Thus for each $a \in E$ there is an extension $t$ of $s$ in $S_q(R,R^\prime)$ such that $a \in \operatorname{dom} (t)$.

Another way to look at it is the following: the connection between $S_p(R,R^\prime)$ and $S_{p+1}(R,R^\prime)$ has absolutely nothing to do with the natural number $p$, but instead just involves the set of partial isomorphisms itself. We could instead define for every family $S$ of local isomorphisms the set $\operatorname{EF}(S)$ (for E​hrenfeucht–F​raïssé) to be the collection of all local isomorphisms which satisfy the Back and Forth conditions with respect to $S$:

$s \in \operatorname{EF}(S)$ iff

*

*for each $a \in E$ there is a $t \in S$ extending $s$ with $a \in \operatorname{dom}(t)$; and

*for each $b \in E^\prime$ there is a $t \in S$ extending $s$ with $b \in \operatorname{ran}(t)$.


It should now be absolutely clear that  $S = T$ implies $\operatorname{EF}(S) = \operatorname{EF}(T)$. Also, by definition $S_{p+1}(R,R^\prime) = \operatorname{EF}(S_p(R,R^\prime))$.
Therefore, if $S_{p}(R,R^\prime) = S_{p+1}(R,R^\prime)$ we will have, for example, that $$S_{p+1}(R,R^\prime) = \operatorname{EF}(S_{p}(R,R^\prime)) = \operatorname{EF}(S_{p+1}(R,R^\prime)) = S_{p+2}(R,R^\prime)$$ and we can continue in this fashion by induction to show that $S_{q}(R,R^\prime) = S_{p}(R,R^\prime)$ for all $q \geq p$.
