Equality reasoning for bisimularity
Proved monotonicity of apply* using ~-Reasoning