λR.λms:metric_space R.λs:sequence ms.λk.λn. δ (s n) k.
notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}.
-interpretation "tends to" 'tends s x = (tends0 _ (d2s _ _ s x)).
+interpretation "tends to" 'tends s x = (tends0 ? (d2s ? ? s x)).