I have a translation function which translates $\lambda$-terms to another representation let me call it $G_\lambda$, as follows.
$\chi(x)$ $=$ $ X^2$ if $ x \notin \Gamma$
$\chi(x)$ $=$ $X$ if $ x:X \in \Gamma $
$\chi(\lambda x.t_1)$ $=$ $abs(X^1,\chi(t_1))$ and do $\Gamma,x:X^1$
$\chi(t_1 \, t_2)$ $=$ $app(\chi(t_1),\chi(t_2))$
where to translate $\chi(\lambda x.t_1)$, it creates a distinct $X^1$ and add a pair $x:X$ to set $\Gamma$.
$\chi(x)$ look $x$ in $\Gamma$, so we can use already added $X^1$ as bound variable or create a distinct $X^2$ for the free variable $x$.
so, a $\lambda$-term $\lambda x.yx$ will be $abs(X^1.app(Y^2,X^1))$.
I think $\chi$ is a bijection. It is obvious that function $\chi$ maps one $\lambda$-term to one $G_\lambda$ representation, so it is injective.
My problem is that since $X^1$ and $X^2$ are created fresh, if you translate a $\lambda$-term $\lambda x.yx$ twice, then you will have two representation such as $abs(X^1.app(Y^2,X^1))$ and $abs(A^1.app(B^2,A^1))$, which are equal terms but not syntactically same.
But how can i prove from $G_\lambda$ to $\lambda$-term is a surjective?