See the discussion at https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/116.

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.