Added '<==>' keyword to transformational proof