how to prove the following is a bijection? 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?
One option could be adding more parameters to $\chi$ so to make both $\Gamma$ and a fresh name source $\phi \in {\sf Names}^\infty$ explicit:

$$
\begin{array}{l}
\chi(\Gamma, x, X;\phi) = X \mbox{ if } x \not\in\Gamma
\\
\chi(\Gamma, x, \phi) = X \mbox{ if } x:X \in\Gamma
\\
\chi(\Gamma, \lambda x. t, X;\phi) = abs(X, \chi(\Gamma;x:X, t, \phi))
\\
\chi(\Gamma, t_1 t_2, \phi) = app(\chi(\Gamma, t_1, \phi^1),\chi(\Gamma, t_2, \phi^2))
\\
\qquad \mbox{where } \phi = \phi^1_0 \phi^2_0 \phi^1_1 \phi^2_1 \phi^1_2 \phi^2_2 \ldots
\end{array}
$$

You can then state a form of injectivity as
$$
\chi(\Gamma, t_1, \phi) = \chi(\Gamma, t_2, \phi) \implies t_1 = t_2
$$
and surjectivity as
$$
\forall T.\ \exists \Gamma, t, \phi.\ \chi(\Gamma, t, \phi) = T
$$

Note that some stronger forms of injectivity do not hold. E.g.
$$
\chi(\Gamma_1, t_1, \phi) = \chi(\Gamma_2, t_2, \phi) \implies \Gamma_1 = \Gamma_2 \land t_1 = t_2
$$
is false since 
$$
\chi(x:X,x, \phi) = \chi(y:X,y, \phi) \land x:X \neq y:X
$$
Similarly, this does not hold:
$$
\chi(\Gamma, t, \phi_1) = \chi(\Gamma, t, \phi_2) \implies \phi_1 = \phi_2
$$
since only a finite portion on $\phi$ is needed by $\chi$.