@jdw I guess this is related to "Dickson's lemma" which has an intuitionistic proof according to [1], with the caveat that [1] talks about infinite sequences rather than well-founded induction.

According to [2, Corollary 2.4], you can show that an ordering R is well-founded by showing that in the classifying topos of "an infinite R-decreasing chain", false holds. This *should* close the gap between your question and the claim in [1], but there is surely a more direct answer. There's quite a lot of literature on this type of "constructive Ramsey theory".

[1] W. Veldman, An intuitionistic proof of Kruskal’s theorem
[2] https://www.speicherleck.de/iblech/stuff/early-draft-modal-multiverse.pdf