Refactor metric-spaces module

[malarbol]

Recent contributions in the metric-spaces modules raise concerns about the names of some concepts in the metric-spaces module.

• refactor pre/pseudo/metric-spaces
• rename indistinguishable --> indiscernible (see comment)

[fredrik-bakke]

Here's a couple more points:

• The divide metric space/metric structure seems a bit over the top. I suggest we factor these to be contained in the same files (and same for premetrics and pseudometrics and any other such divides in this namespace).
• The concept of indistinguishability should be factored to separate files, called similarty-of-elements-metric-spaces and so on. This is consistent with other notions of similarity in the library.
• The definition of indistinguishability in premetric spaces is not the correct one, it only applies to (reflexive?) symmetric premetric spaces. I propose we forget the non pseudo- case and only first define similarity for pseudometric spaces.

[fredrik-bakke]

For future reference, the correct similarity relation on premetric spaces is probably

(x ≍ y) :=
  ((ε : ℚ⁺) → (B ε x x ↔ B ε y y)) ×
  ((ε : ℚ⁺) (z : A) → (B ε x z ↔ B ε y z)) ×
  ((ε : ℚ⁺) (z : A) → (B ε z x ↔ B ε z y))