This paper concerns itself with correct by construction refactoring of Maybe values to List values in a Haskell-like language (HLL) as a case study on data-oriented refactorings. Our language makes use of intrinsically-typed syntax and de Bruijn indices for variables. Operational semantics are defined using big step semantics. We define a refactoring function which intrinsically verifies its well-typedness due to our intrinsically-typed syntax. The semantic validity of this refactoring is given by a separate proof. We use Agda, a functional language and theorem prover, to define and prove these properties. Techniques and concepts used in our refactoring and proof generalize well to other data-oriented refactorings.