take <* the 1-sorted *> ; :: thesis: ( <* the 1-sorted *> is FinSequence-like & <* the 1-sorted *> is 1-sorted-yielding )
thus ( <* the 1-sorted *> is FinSequence-like & <* the 1-sorted *> is 1-sorted-yielding ) ; :: thesis: verum