An old proof of the wellfoundednes of the multiset ordering

The proof that the multisets ordering preserves wellfoundedness that I posted
here on Monday had already been discovered by Thierry Coquand. He told me

> I had a similar argument in An Analysis of Ramsey Theorem, Information
> and Computation 110, 1994, p. 297-304. This is lemma 7 (at the end
> in the remarks, I point out that this can be used for proving that
> a multiset extension of a wf relation is wf).