The syntactic logical relations developed by Pitts are applied to show the correctness of a higher-order removal program transformation algorithm. The convenient proof method that resorts to the induction on the structure of programs does not apply because of the circular references to be introduced by the transformation. Using a variant of the syntactic logical relations, in which every pair of the transformation source and target are related, one can break the circularity and make an inductive proof go through. This demonstrates that the syntactic logical relations provide a basis of another general proof method for showing the correctness of program transformations.