Given and(goal_a, goal_b), previously if goal_b could produce an
infinite number of solutions, then goal_a wouldn't get a chance to move
on the to previous. It was doing a sort of dependent Cartesian product
where it would take one step on goal_a in order to find the context for
goal_b, and then completely exhaust goal_b in that context.
Now, we do a diagonal search, keeping a vector of searches in goal_b,
and asking goal_a for a new context each time we loop back around to the
beginning. If goal_a is exhausted, we stop adding new searches, and if
any of the searches in goal_b is exhausted, we remove it from the list
of searches to iterate over.
Some specific things to note: we respect yields in goal_a, so that a
diverging goal_a doesn't get stuck and instead will repeatedly yield,
letting the rest of the program continue its search, interleaved
elsewhere.
This changes performance, making the large Peano addition slower.