λxs.λys.
  { succDiff ← ((-)\~)
  ; (+)/([√(x^2+y^2)]`(succDiff xs) (succDiff ys))
  }