The undecidability of simultaneous rigid E-unification with two variables

Recently it was proved that the problem of simultaneous rigid E-unification, or SREU, is undecidable. Here we show that 4 rigid equations with ground left-hand sides and 2 variables already imply undecidability. As a corollary we improve the undecidability result of the ∃*-fragInent of intuitionistic logic with equality. Our proof shows undecidability of a very restricted subset of the ∃∃-fragment. Together with other results, it contributes to a complete characterization of decidability of the prenex fragment of intuitionistic logic with equality, in terms of the quantifier prefix.