Make use of curly braces, adjust indentation.
Split the proof of bisimulation again (this is much faster).