In their article "A Borsuk-Ulam Equivalent that Directly Implies Sperner's Lemma" (American Mathematical Monthly, April 2013), Nyman and Su write "[W]e are unaware of a direct proof that Tucker's lemma implies Sperner's lemma".

Could there be a mathematical obstruction to finding a derivation of Sperner's lemma from Tucker's lemma? E.g., could there be a mathematical context (perhaps some fragment of ZF as a background theory), and in that context two propositions S and T that are recognizable as versions of Sperner's lemma and Tucker's lemma, such that T is true but S is false? Or a computational context in which finding "Sperner's maguffin" (a fully labeled n-simplex) is demonstrably harder than finding "Tucker's maguffin" (a complementary edge)?

See the related thread In what rigorous sense are Sperner's Lemma and the Brouwer Fixed Point Theorem equivalent?.