When designing critical software, great care must be taken to guarantee its correctness. Refactoring is one of the techniques used to improve code readability, maintainability, and other factors without changing functionality. Thus, to ensure that it is properly applied, automated tools are used to perform refactoring. To ensure that the code remained correct, we verified the correctness of the tool actions using formal proof. This is assisted by a dependently typed language Agda, which, when used as a proof assistant, can directly support us by ensuring the soundness of the steps taken. We consider the refactoring of currying and its counterpart, uncurrying, using a small proof-of-concept functional programming language with intrinsically typed terms and de Bruijn indices. Furthermore, we proved the retained properties of well-typedness, termination, and value relation of the input program. Finally, we argue that this research could be extended to the full implementation of Haskell, as well as applied to other languages and similar refactorings.