- ∀R.∀ml:mlattice R.∀xn:sequence ml.
- ∀x,y:apart_of_metric_space ? ml.
- (* BUG: it inserts a compesoed coercion instead of an hand made one,
- what to do? prefer the human made one or allow to kill a coercion?
- *)
- xn ⇝ x → xn ⇝ y → x ≈ y.
+ ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x,y:ml.
+ xn ⇝ x → xn ⇝ y → δ x y ≈ 0.