Goal A -> B.
intro.
Undo.
Undo.
Undo.
Undo.