二阶单射存在左逆的证明求助

我卡在这个问题上好几天了，想请教各位怎么证明二阶逻辑里的单射存在左逆，先跟大家理清楚背景和我的思路：

背景：一阶单射的左逆性质 #

我们知道在集合论里，每个单射都有左逆，也就是下面这两个命题等价：
$$\forall x,y(f(x)=f(y)\implies x=y)$$
当且仅当
$$\exists g:\text{im}(f)\to\text{dom}(f)\forall x(g\circ f(x)=x)$$

我的目标：二阶单射的等价性质 #

现在我想证明**二阶“单射”**也有类似的等价关系：
$$\forall x,y(Fx=Fy\implies x=y)$$
当且仅当
$$\exists_FG\forall x(GFx=x)$$

可用的证明工具 #

我手头能用的工具有这些：

• 选择公理：
  $$\forall_PP(\forall x\exists yPxy\implies \exists_FF\forall xPxFx)$$
• 偏函数定理：
  $$\forall_P P,Q(\forall x(Px\implies \exists yQxy)\implies\exists_FF \forall x(Px\implies QxFx))$$
• 唯一函数定理：
  $$\forall_PP(\forall x\exists! yPxy\implies\exists!_FF\forall xPxFx)$$
• 满射等价于存在右逆定理：
  $$\forall_FF(\forall x\exists y(Fy=x)\iff\exists_F G\forall x(FGx=x))$$
• 概括公理：
  $$\exists_PP\forall\langle x\rangle_n(P^n\langle x\rangle_n\iff\Phi\langle x\rangle_n)$$
  其中$\Phi$是任意公式，$\langle x\rangle_n$是$n$个变量。

另外，所有带等词的一阶逻辑公理都是可证的。这是我自己的学习研究，不确定这个结论是不是一定可证，但二阶逻辑相关的资料太少了，不管是思路还是提示，相信都会帮到很多和我一样的学习者。

我的证明尝试（卡壳点） #

首先假设二阶单射的条件：
$$Fx=Fy\implies x=y$$

我通过一阶逻辑知道，对任意变量$x$，存在某个$c$使得$x=c$，由此可以推出：
$$Fx=y\implies x=c$$

接着用概括公理定义一个谓词$Pyz$，然后通过存在推广得到$\exists zPyz$，再全称推广得到$\forall y\exists zPyz$，这时候我用选择公理得到：
$$\exists_FG\forall yPyGy$$

把它转成公式就是：
$$\forall y(Fx=y\implies x=Gy)$$

然后我令$y=Fx$，代入后得到：
$$Fx=Fx\implies x=GFx$$
由此可以推出$x=GFx$，也就是$GFx=x$。

接下来我做了存在推广得到$\exists_FG(GFx=x)$，再全称推广得到：
$$\forall x\exists_FG(GFx=x)$$

问题就在这里！ 我需要的是$\exists_F G\forall x(GFx=x)$——也就是存在一个统一的G对所有x都满足$GFx=x$，而不是上面这个“对每个x都存在一个可能不同的G”的形式。我知道肯定要用到最开始的单射假设，但就是不知道怎么把这个量词顺序从“$\forall x\exists_FG$”转换成“$\exists_FG\forall x$”。

另外我还证出了一个结论：
$$\forall x(\exists_y(Fy=x)\iff \exists!y(Fy=x))$$
感觉这个结论可能有用，但不知道怎么结合它往下走，实在卡壳了，希望能得到大家的帮助！

备注：内容来源于stack exchange，提问作者Isaac Sechslingloff