Solution for Himpl.XsimplTactic.xchange_lemma
Click on the 'Next' button to reveal the proof step by step.