Implement a typing rule for saturated seq, and document it