I have a tactic, lets call it
branch which creates, some number of goals. I have another tactic, let’s call it
solve that solves the goal if there is enough information in the context. I want to apply combination of tactics in a depth-first manner. In other words, I want to
try solve new goals, then
branch in first goal only. Do this recursively until that branch of goal tree is solved, then jump into the next first goal. How can I achieve this?