Are all group monomorphisms regular, constructively?

By "constructive" I mean something that would go through in CZF for example.

[added Oct 6] A sketch of a standard proof (such as referenced in comment below), which is almost constructive: Let H be a subgroup of G, and consider the (say, left-) cosets of H, plus a distinguished element. There is a homomorphism f from G to the permutation group of these, given by left multiplication (leaving the extra element fixed). Construct an involution t which exchanges the coset of 1 and the distinguished element. Then for all g in G, f(g) = t.f(g).t iff g is in H.

The involution t distinguishes the coset of 1 from the other cosets. In other words t can distinguish elements of G which are in H from those which aren't. So in CZF we have the theorem: every "detachable" subgroup H of G is the equaliser of two group homomorphisms. That is, this seems to require the additional hypothesis that $\forall x \in G (x \in H \vee x \not\in H)$. Of course this is a classical tautology so it disappears when we go to ZF (which is CZF + law of excluded middle).

[end of addition]

In practice, an answer to the following question will probably yield an answer (and if it fails to, it will probably be for an interesting reason)

I call a PER-Group a subset G of natural numbers, and equivalence relation R on G, with multiplication and inverse operations as partial computable functions, totally defined over G, and respecting R.

Note G and R need not even be c.e. [and in fact, if H is a decidable subset of G, then the problem is already solved, as above] For instance, addition over the computable reals is computable, even though the set of codes for computable reals is not c.e., nor is equality of two computable reals. Of course that example is abelian, and the proof that every abelian group monomorphism is normal is constructive. I am interested in the non-abelian case.

Is every PER-group inclusion the equaliser of two PER-group homomorphisms?