mreflexive: ∀a. metric a a ≈ 0;
msymmetric: ∀a,b. metric a b ≈ metric b a;
mtineq: ∀a,b,c:ms_carr. metric a b ≤ metric a c + metric c b
mreflexive: ∀a. metric a a ≈ 0;
msymmetric: ∀a,b. metric a b ≈ metric b a;
mtineq: ∀a,b,c:ms_carr. metric a b ≤ metric a c + metric c b