Definition CR := Complete Q_as_MetricSpace.


Definition inject_Q : Q -> CR := (@Cunit Q_as_MetricSpace).


Notation "' x" := (inject_Q x) : CR_scope.

Notation "x == y" := (@st_eq CR x y) (at level 70, no associativity) : CR_scope.