Refactoring tools are an important tool for developers, but their reliability can be questionable at times. In this paper, we show that it is feasible to formally verify refactoring tools using computer-aided proofs. To this end, we create a Haskell-like language and a refactoring operation on this language to add an extra function argument to an arbitrary function in the program. And finally, use the Agda proof assistant to construct a proof of the correctness of this refactoring.