take {} ; :: thesis: {} is XFinSequence-yielding
thus {} is XFinSequence-yielding ; :: thesis: verum