Problem #5 Template

This problem is taken from Coquand and Spiwack’s Constructively Finite?.

In this problem we will continue to investigate properties of finite sets. Call a set X streamless if every sequence f : nat -> X repeats itself at two points.

While being streamless captures an intuitive notion of finiteness, it is, as discussed in the article, weaker than other finiteness notions. Nonetheless, we can still prove that streamlessness satisfies some properties which we would expect a notion of finitness to hold:

Problem: Show that the streamless sets are closed under taking disjoint unions.