Chasing the goal entering backward while interpreting tactics. This required
writing a new primitive recovering the first goal under focus. It sounds a bit
hackish, but it does actually work.