Source-level transformations of programs are fundamental to achieve high-performance: complex loop transformations, including loop tiling and parallelization, must typically be applied by a user or an automated tool. However this process is error-prone, especially when combined with transformations of the data layout, code structure and statements themselves. In this work, we present an approach to prove the equivalence between a function and its candidate optimized version which is mostly agnostic to the schedule and storage implemented. It can prove the equivalence between a sequential function and its parallelized version, under practical restrictions.