GitLab

Also make the instances non-global, to prevent multiple instance
problems.

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.

This implements a simple linear search for fresh elements.

This generalizes Fix_unfold to a setoid setting. In particular,
we can use this to unfold multi-argument fixpoints without
requiring functional extensionality.

Infinity is described by having an injection from nat.

The documentation for some typeclasses used the wrong
names for these typeclasses.

This addresses some concerns in !5.

This way, we will be compabile with Iris's heap_lang, which puts ;;
at level 100.

This fixes the issue of Hai in !6.

This allows for more control over `Hint Mode`.

This way, type class search will fail immediately on first type
class constraint of any of the `fin_map_dom` lemmas if no `Dom`
can be found.