  In reverse mathematics, is is possible to have a curious situation where we
know that an implication does not reverse, but appear to have no information on
on how to weaken the assumption while preserving the conclusion. A main cause
of this phenomenon is the proof of a $\Pi^1_2$ sentence from the theory
{\Pioo}. Using methods based on the functional interpretation, we introduce a
family of weakenings of {\Pioo} and use them to give new upper bounds for the
Nash-Williams Theorem of wqo theory and Menger's Theorem for countable graphs.
