Add a segment-segment length equality

This is either a point-point-point-point distance equality (between two pairs of points), or perhaps we actually abstract over this with a segment. Note a segment is not the same as an infinite line. A segment and two pairs of points are conceptually exactly the same, whereas a line is (over-)defined by two pairs of points.