Formalizing the meta-theory of program equivalences in Coq