We claim that $f\colon S\to \{E,N\}$ defined by $f(\tuple s)=O_{\tuple s}$ is a solution to the finite injectivisation of $\instance$ on $S$.
To this end, let $C\in\constraints$ and let $g'\in C$ be monotone and injective. It follows that $p_1'(g,g')\in C$ and moreover, $O(p_1'(g(\tuple s),g'(\tuple s))=O_{\tuple s}$ for all $\tuple s\in S$ such that all variables from $\tuple s$ are in the scope of $C$ and the lemma follows.
\end{proof}

\begin{lemma}\label{lemma:ppdef}
Let $\instance=(\V,\constraints)$ be a $(2\ell,\max(3\ell,b_{\mathbb H}))$-minimal, non-trivial, $\textrm{eq}$-subdirect instance of $\CSP(\mathbb A)$ such that $\proj_{(u,v)}(\instance)\cap I_2\neq\emptyset$ for every $u\neq v\in\V$. Let $S\subseteq\injtuples$ and let $\{E^{i}_{\tuple s}\mid \tuple s\in S, i\in [m]\}$ be sets of classes of the partitions from the algorithm. Suppose that there exists $\tuple s'\in S$ such that the relation $\bigcup\limits_{i\in\{2,\ldots, m\}}E^i_{\tuple s'}$ is not preserved by $p_1$ or by $m$. Then the finite injectivisation of $\instance$ on $S$ has a solution.
\end{lemma}
\begin{proof}
Suppose that the relation $R:=\bigcup\limits_{i\in\{2,\ldots, m\}}E^i_{\tuple s'}$ is not preserved by $p_1$. Let $\tuple a_1, \tuple a_2\in R$ be such that $p_1(\tuple a_1,\tuple a_2)\in E^1_{\tuple s'}$.

For $j\in[2]$, let $O^j$ be the orbit of $\tuple a_j$ under $\Aut(\mathbb H)$. Let $h^j\colon \V\to H$ be a solution to $(\instance^{\tuple s'\in O^j})_{\textrm{eq}}$ such that $h^j(\tuple s')=\tuple a_j$.
Let $h:=p_1(h^1,h^2)$.
It follows that $h(\tuple s')\in E^1_{\tuple s'}$ and, by the way how the partitions are obtained, $h(\tuple s)\in E^1_{\tuple s}$ for every $\tuple s\in S$. In particular, $h(\tuple s)$ lies in an injective or deterministic under $\Aut(\mathbb H)$ for every $\tuple s\in S$.

Let $\tuple s_1,\ldots,\tuple s_n$ be all tuples in $S$ such that $h(\tuple s_i)$ is not injective. For every $i\in [n]$, let $\beta_i\in \Aut(\mathbb H)$ be such that $\beta_i$ is deterministic for $h(\tuple s_i)$.
Let now $p''_1(x,y):=p_1(\beta_1 x,p_1(\beta_2 x,p_1(\ldots,p_1(\beta_n x,y))\dots))$.
Observe that for all $\tuple s\in S$, we have that $p''_1(O_<(h(\tuple s)),E)$ and $p''_1(O_<(h(\tuple s)),N)$ are subsets of the same orbit $O_{\tuple s}\in\{E,N\}$ under $\Aut(\mathbb H)$.
Let $f\colon S\to\{E,N\}$ be defined as $f(\tuple s)=O_{\tuple s}$.
We claim that $f$ is a solution of the finite injectivisation of $\instance$ on $S$.

To this end, let $C\in \constraints$. By the choice of $h^1,h^2$, there exist $g^1,g^2\in C$ ordered by $h^1$ and $h^2$, respectively, It follows that $g:=p_1(g^1,g^2)$ is ordered by $h$ and moreover, $g\in C$. For every $i\in[n]$, let $\alpha_i\in\Aut(\mathbb H)$ be such that $\alpha_i g$ is ordered by $\beta_i h$. Let $p'_1(x,y):=p_1(\alpha_1 x,p_1(\alpha_2 x,p_1(\ldots,p_1(\alpha_n x,y))\dots))$ and let $g'\in C$ be monotone and injective. It follows that for every $\tuple s\in S$ such that all variables from $\tuple s$ are contained in the scope of $C$ and for every $i\in[n]$, $O_<(\alpha_i g(\tuple s))=O_<(\beta_i h(\tuple s))$. In particular, $p_1'(g(\tuple s),g'(\tuple s))\in f(\tuple s)$ as desired.

The case when $R$ is not preserved by $m$ is similar.
\end{proof}

Using the auxiliary statements above, we are able to prove the correctness of the main algorithm:

\begin{theorem}\label{thm:algorithm_correct}
The instance $\instance'$ produced by the algorithm in~\Cref{alg:inj-irreducibility} is an instance of $\CSP(\mathbb A)$ and it has a solution if, and only if, the original instance has a solution.
Moreover, $\instance'$ is either trivial or inj-irreducible.
\end{theorem}

\begin{proof}
It is easy to see that $\instance'$ is an instance of $\CSP(\mathbb A)$ by the algorithm -- the only thing that needs to be proven is that if the algorithm constrains an injective tuple $\tuple v\in\V^{\ell}$ by $\proj_{\tuple v}(\instance)\backslash E^1_{\tuple v}$, where $\instance=(\V,\constraints)$ is an $\textrm{eq}$-subdirect, $(2\ell,\max(3\ell,b_{\mathbb H}))$-minimal instance obtained during the run of the algorithm, then $\proj_{\tuple v}(\instance)\backslash E^1_{\tuple v}$ is preserved by $p_1$ and by $m$. But this follows directly from~\Cref{lemma:ppdef}.

We will now show that if the original instance has a solution, the instance $\instance'$ has a solution as well. Suppose that in the repeat... until not changed loop, we get an instance $\instance=(\V,\constraints)$ and we removed a solution of $\instance$ during one run of this loop. Clearly, we didn't remove any solutions by making the instance $\textrm{eq}$-subdirect, $(2\ell,\max(3\ell,b_{\mathbb H}))$-minimal and by identifying variables in the \textsc{IdentifyAllEqual} subroutine. Hence, the only problem could occur when removing the classes $E^1_{\tuple w}$.

Suppose therefore that there is a set $S\subseteq \injtuples$ and a partition $\{E^j_{\tuple v}\mid j\in \{1,\ldots,m\}, \tuple v\in S\}$ on the projections of $\instance$ to the tuples from $S$. Suppose moreover that $\instance$ had a solution $s\colon \V\to H$ such that $s(\tuple w)\in E^1_{\tuple w}$ for some $\tuple w\in S$. Then $s(\tuple v)\in E^1_{\tuple v}$ for every $\tuple v\in S$ by the definition of the partition.

Recall that $E^1_{\tuple v}$ contains all injective orbits under $\Aut(\mathbb H)$ that are contained in $\proj_{\tuple v}(\instance)$ for all tuples $\tuple v\in S$ by the reasoning below the algorithm. Let $\instance''$ be an $\ell$-minimal instance equivalent to the instance obtained from $\instance$ by adding for every $\tuple v=(v_1,\ldots,v_{\ell})\in S$ the constraint $\{g\colon \{v_1,\ldots,v_{\ell}\} \rightarrow H\mid g(\tuple v)\in E^1_{\tuple v}\}$.
Since $E^1_{\tuple v}$ is pp-definable in $\mathbb A$, it is by assumption one of the relations of $\mathbb A$ and therefore $\instance''$ is an instance of $\CSP(\mathbb A)$.
Since $s$ is a solution to $\instance$ and hence also to $\instance''$, $\instance''$ is non-trivial.
Since the classes $\{E^1_{\tuple v}\mid \tuple v\in S\}$ were removed, the finite injectivisation of $\instance$ on $S$ does not have a solution and it follows that the finite injectivisation of $\instance''$ on $S$ does not have a solution as well. Hence, $s$ is not a solution to $\instance''$ by~\Cref{lemma:NoSolutionRem