Formalizing Program Equivalences in Dependent Type Theory