take cs ; :: thesis: cs is constant
thus cs is constant ; :: thesis: verum