Fresh renaming

Given a set of variables $\\mathcal{X}$ and a finite sequence of variables $\\vec{x}$, a bijection $\\rho : \\vec{x} \\leftrightarrow \\vec{x}'$ between $\\vec{x}$ and $\\vec{x}'$, where $\\vec{x}'$ is fresh f

Given a set of variables $\mathcal{X}$ and a finite sequence of variables $\vec{x}$, a bijection $\rho : \vec{x} \leftrightarrow \vec{x}'$ between $\vec{x}$ and $\vec{x}'$, where $\vec{x}'$ is fresh for $\mathcal{X}$.