In "Calculational Design of A Regular Model Checker by Abstract Interpretation" by Patrick Cousot (link), on page 15 it can be seen that to prove the completeness of regular model checking (Definition 12) with respect to model checking (Definition 7), Cousot is trying to prove this proposition in Lemma 15:
$$\{\underline \rho \} \times \mathcal{S}^* [ \mathsf{P}] \subseteq \mathsf{prefix}(\mathcal{S}^r[\mathsf{R}\bullet(?:\mathit{T})^*]) \Rightarrow \mathcal{S}^* [ \mathsf{P}] \subseteq \mathcal{M}[\mathsf{P}]\mathsf{R} $$
I think that the given proof does not prove this proposition, but it proves the reverse of this proposition instead, which has been proved in Lemma 14.
Does anyone agree with me? Or am I getting something wrong here?
Also, I think that the statement of Lemma 14 is wrong. First, I have not seen the definition of $\mathcal{M}$ that does not take $\underline{\rho}$ (an initial environment) in the paper, and second, if we assume that $\mathcal{M}[\mathsf{P}] \mathsf{R}$ is an abbreviation of $\mathcal{M}[\mathsf{P}] \langle \underline{\rho}, \mathsf{R}\rangle$ (which is defined) then it should be considered that $\mathcal{M}[\mathsf{P}] \langle \underline{\rho}, \mathsf{R}\rangle$ contains $\pi$ (prefix traces) while $\mathsf{prefix}(\mathcal{S}^r [\mathsf{R}\bullet(?:\mathit{T})^*])$ contains $\langle \underline{\rho},\pi \rangle$ (pairs consisting of an initial environment and a prefix trace), so they are not comparable or in other words, the inclusion never holds.
