[Agda] Kruskal's theorem

[Sergei Meshveliani]

People,

consider the following theorem.

Th-0
----
Let   w(1), w(2) ...   
be an infinite sequence of words in the alphabet  {a, b}.
Then there exist  i < j  such that  w(i) is a subword in w(j)
(that is   w(j) = u w(i) v   for some words  u, v).

1) Is this true?
(I am sorry if I confuse things).

2) Is this a special case of Kruskal's theorem about finite trees?
3) Has anybody tried to prove in Agda a theorem like Th-0 ?
4) In Coq ?

Thanks,

------
Sergei