Relational program logic

This is a formalization of the paper The next 700 relational program logics.

We follow the paper as well as the Coq formalization in SSProve.