-
Dan Frumin authored
- 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
f638d4f9