- Define several versios of bind and return for the relational
  interpretation
- Use those operations to prove some compatibility lemmas
  without unfolding the definitions
- Get rid of the definition unfolding in a part of the stack
  refinement proof