We prove that various types are infinite, notably:
- nat, N, positive and Z;
- string (using pretty-printing of nat);
- option, with an infinite element type;
- list, with an inhabited element type.

Furthermore, we instantiate Fresh for strings.